English
For rationals p and q, p = q if and only if p.num × q.den = q.num × p.den.
Русский
Для дробей p и q верно: p = q тогда и только тогда, когда p.num × q.den = q.num × p.den.
LaTeX
$${p,q : \mathbb{Q}} \; : \; p = q \iff p.num \cdot q.den = q.num \cdot p.den$$
Lean4
theorem eq_iff_mul_eq_mul {p q : ℚ} : p = q ↔ p.num * q.den = q.num * p.den :=
by
conv =>
lhs
rw [← num_divInt_den p, ← num_divInt_den q]
apply Rat.divInt_eq_divInt_iff <;>
· rw [← Int.natCast_zero, Ne, Int.ofNat_inj]
apply den_nz