num_mul_eq_mul_denom_iff — Mathlib

English

For q ≠ 0, x = p/q iff x.num · q = p · x.denom.

Русский

При q ≠ 0 верно: x = p/q, тогда x.num · q = p · x.denom.

LaTeX

$$$\text{If } q \neq 0:\; x = \dfrac{p}{q} \iff x.num \cdot q = p \cdot x.denom$$$

Lean4

theorem num_mul_eq_mul_denom_iff {x : RatFunc K} {p q : K[X]} (hq : q ≠ 0) :
    x.num * q = p * x.denom ↔ x = algebraMap _ _ p / algebraMap _ _ q :=
  by
  rw [← (algebraMap_injective K).eq_iff, eq_div_iff (algebraMap_ne_zero hq)]
  conv_rhs => rw [← num_div_denom x]
  rw [RingHom.map_mul, RingHom.map_mul, div_eq_mul_inv, mul_assoc, mul_comm (Inv.inv _), ← mul_assoc, ← div_eq_mul_inv,
    div_eq_iff]
  exact algebraMap_ne_zero (denom_ne_zero x)

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