Submission Details

Back to Submissions List

Challenge: solveMul

Submitted by: kvanvels

Submitted at: 2024-11-15 18:09:04

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
  rintro ⟨p,h0⟩
  unfold solveMul
  split_ifs with h1
  exfalso
  rw [h1,zero_mul] at h0
  linarith
  exact mul_one_div_cancel h1

Status: Correct

Feedback:

Second Theorem Proof:

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

:= by
  rintro noS
  unfold solveMul
  split_ifs with h1
  rfl
  by_contra
  apply noS
  use (1/a)
  exact mul_one_div_cancel h1
  

Status: Incorrect