div_eq_div_iff_div_eq_div' — Mathlib

English

In a commutative group with zero, a/b = c/d ↔ a/c = b/d, provided b,c ≠ 0.

Русский

В коммутативной группе с нулём: a/b = c/d эквивалентно a/c = b/d при b ≠ 0 и c ≠ 0.

LaTeX

$$$\forall b,c\neq 0:\; a/b=c/d \iff a/c=b/d$$$

Lean4

/-- The `CommGroupWithZero` version of `div_eq_div_iff_div_eq_div`. -/
theorem div_eq_div_iff_div_eq_div' (hb : b ≠ 0) (hc : c ≠ 0) : a / b = c / d ↔ a / c = b / d :=
  by
  conv_lhs => rw [← mul_left_inj' hb, div_mul_cancel₀ _ hb]
  conv_rhs => rw [← mul_left_inj' hc, div_mul_cancel₀ _ hc]
  rw [mul_comm _ c, div_mul_eq_mul_div, mul_div_assoc]

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