Submission Details

Back to Submissions List

Challenge: solveMul

Submitted by: GasStationManager

Submitted at: 2024-11-16 08:46:38

Code:

import Mathlib.Data.Rat.Defs

def solveMul(a: Rat): Rat

:= if a=0 then 0 else 1/a

First Theorem Proof:

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

:= by
    intro h
    simp[solveMul]
    split
    next ha=>
      simp[ha] at h
    next ha=>
      exact Rat.mul_inv_cancel a ha

Status: Correct

Feedback:

Second Theorem Proof:

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

:= by
    intro h
    simp[solveMul]
    contrapose! h
    use 1/a
    exact mul_one_div_cancel h

Status: Correct