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']⟩