Submission Details

Back to Submissions List

Challenge: solveMul

Submitted by: Violeta Hernández Palacios

Submitted at: 2024-11-19 09:17:08

Code:

import Mathlib.Data.Rat.Defs

def solveMul(a: Rat): Rat

:=a⁻¹

First Theorem Proof:

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

:=by
  simp [solveMul]
  intro x hx
  apply Rat.mul_inv_cancel a 
  rintro rfl
  simp at hx

Status: Correct

Feedback:

Second Theorem Proof:

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

:= by
  simp [solveMul]
  contrapose! 
  intro h
  use a⁻¹
  exact Rat.mul_inv_cancel a h

Status: Correct