solveDiv

write a function that, given rationals a and b, both not equal to zero, return x such that a/x=b.

Function Signature

import Mathlib.Data.Rat.Defs

def solveDiv(a b:Rat) (ha: a≠ 0)(hb: b≠ 0): Rat

Theorem Signature

theorem solveDiv_correct(a b:Rat)(ha:a≠ 0)(hb: b≠ 0):
a / (solveDiv a b ha hb)= b

View All Submissions

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