solveMul

write a function that, given rational a, returns a rational x such that a*x=1. If no solution exists, return 0.

Function Signature

import Mathlib.Data.Rat.Defs

def solveMul(a: Rat): Rat

Theorem Signature

theorem solveMul_correct(a:Rat): (∃ x, a*x=1)->a * (solveMul a)=1

Additional Theorem Signature

theorem solveMul_nosol (a:Rat): (Not (∃ x, a*x=1)) ->solveMul a =0

View All Submissions

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