Submission Details

Back to Submissions List

Challenge: solveDiv

Submitted by: kvanvels_2

Submitted at: 2024-11-19 01:33:29

Code:

import Mathlib.Data.Rat.Defs

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: Correct

Feedback:

/tmp/tmp5nej8_90/proof.lean:4:23: warning: unused variable `ha`
note: this linter can be disabled with `set_option linter.unusedVariables false`
/tmp/tmp5nej8_90/proof.lean:4:33: warning: unused variable `hb`
note: this linter can be disabled with `set_option linter.unusedVariables false`