solve1x1

write a function that, given rationals a and b, return some x such that a*x=b. if no solution exists, return none

Function Signature

import Mathlib.Data.Rat.Defs

def solve1x1(a b: Rat): Option Rat

Theorem Signature

theorem solve1x1_correct(a b:Rat): (∃ x, a*x=b) -> a * (solve1x1 a b).get! =b

Additional Theorem Signature

theorem solve1x1_none(a b:Rat): (Not (∃ x, a*x=b)) -> solve1x1 a b=none

View All Submissions

Please log in or register to submit a solution for this challenge.