div_eq_div_iff — Mathlib

English

Let a,b,c,d ∈ ℝ≥0∞ with a ≠ 0, a ≠ ∞, b ≠ 0, b ≠ ∞. Then c/b = d/a if and only if a c = b d.

Русский

Пусть a,b,c,d ∈ ℝ≥0∞ такие, что a ≠ 0, a ≠ ∞, b ≠ 0, b ≠ ∞. Тогда c/b = d/a тогда эквивалентно a c = b d.

LaTeX

$$$$\forall a,b,c,d \in \mathbb{R}_{\ge 0}^{\infty},\ a \neq 0,\ a \neq \infty,\ b \neq 0,\ b \neq \infty \Rightarrow \frac{c}{b} = \frac{d}{a} \iff a c = b d.$$$$

Lean4

protected theorem div_eq_div_iff (ha : a ≠ 0) (ha' : a ≠ ∞) (hb : b ≠ 0) (hb' : b ≠ ∞) :
    c / b = d / a ↔ a * c = b * d := by
  rw [eq_div_iff ha ha']
  conv_rhs => rw [eq_comm]
  rw [← eq_div_iff hb hb', mul_div_assoc, eq_comm]

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