rat.mul_eq

Stream: Is there code for X?

[Patrick Johnson]

Is this (or similar) lemma in mathlib?

example {a b : ℚ} : a * b = a * b.num / b.denom :=
begin
  sorry
end

[Alex J. Best]

I don't think you can do much closer than

import data.rat.basic
lemma a {a b : ℚ} : a * b = a * b.num / b.denom :=
begin
  nth_rewrite 0 ← rat.num_div_denom b,
  rw mul_div_assoc,
end

[Alex J. Best]

I wouldn't think the explicit lemma you wrote with the multiplication and division assoc'd would be added to mathlib as a standalone lemma