eq_div_iff — Mathlib

English

Equivalently, b = c/a iff a*b = c (under nonzero/noninfinity).

Русский

Эквивалентно, b = c/a эквивалентно a*b = c (при ненулевости и не бесконечности).

LaTeX

$$$b = c/a \\iff a b = c \\quad (a \\neq 0, a \\neq \\infty)$$$

Lean4

theorem eq_div_iff (ha : a ≠ 0) (ha' : a ≠ ∞) : b = c / a ↔ a * b = c :=
  ⟨fun h => by rw [h, ENNReal.mul_div_cancel ha ha'], fun h => by
    rw [← h, mul_div_assoc, ENNReal.mul_div_cancel ha ha']⟩

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