Submission Details

Back to Submissions List

Challenge: solveDiv

Submitted by: kvanvels_2

Submitted at: 2024-11-19 01:32:59

Code:

import Mathlib.Data.Rat.Defs

def solveDiv(a b:Rat) (ha: a≠ 0)(hb: b≠ 0): Rat

def solveDiv(a b:Rat) (ha: a≠ 0)(hb: b≠ 0): Rat
:=  a/b

First Theorem Proof:

theorem solveDiv_correct(a b:Rat)(ha:a≠ 0)(hb: b≠ 0):
a / (solveDiv a b ha hb)= b

:= by
  unfold solveDiv
  ring_nf
  rw [inv_inv]
  have h1 : (a * a⁻¹) = (1:Rat) := by exact Rat.mul_inv_cancel a ha
  rw [h1,one_mul]

Status: Incorrect

Feedback:

/tmp/tmp9rhzol82/code.lean:4:47: error: unexpected token 'def'; expected ':=', 'where' or '|'
/tmp/tmp9rhzol82/code.lean:5:4: error: 'solveDiv' has already been declared