eq_iff_mul_eq_mul — Mathlib

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

Похожие утверждения