product of reciprocal fractions is one

Stream: Is there code for X?

[Roman Bacik]

I am new to lean4 and have trouble showing:

lemma mult_rec_is_one (m : ℕ)(n : ℕ)(hm : 0 < m)(hn : 0 < n) : (m/n)*(n/m) = 1 := by
  sorry

Is there already a code for it?

[Roman Bacik]

Got it:

lemma mult_rec_is_one (m : ℕ)(n : ℕ)(hm : 0 < m)(hn : 0 < n) : (m/n : ℚ)*(n/m : ℚ) = 1 := by
  field_simp

[Richard Copley]

(The tactic slim_check will give you a counterexample for the lemma as originally stated.)

[Roman Bacik]

Thank you very much, this slim_check seems to be very helpful.

[Junyan Xu]

@loogle (?a / ?b) * (?b / ?a) = 1

[loogle]

:shrug: nothing found