Submission Details

Back to Submissions List

Challenge: solveMul

Submitted by: kvanvels_2

Submitted at: 2024-11-19 01:26:37

Code:

import Mathlib.Data.Rat.Defs

def solveMul(a: Rat): Rat

:= if(a = 0) then (0 : Rat) else (1:Rat)/a

First Theorem Proof:

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

:= by
  rintro ⟨ainv,h0⟩
  have h1 : ¬(a = 0) := by
    intro htemp
    rw [htemp,zero_mul] at h0
    linarith
  unfold solveMul
  split_ifs with _
  exact mul_one_div_cancel h1

Status: Correct

Feedback:

/tmp/tmp7me2ka4y/proof.lean:15:17: warning: unused name: _

Second Theorem Proof:

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

 := by
  intro h0
  unfold solveMul
  split_ifs with h1
  rfl
  exfalso
  apply h0
  use 1/a
  exact mul_one_div_cancel h1

Status: Correct