div_eq_div_iff_mul_eq_mul — Mathlib

English

Let G be a commutative group. For all a, b, c, d ∈ G, a / b = c / d iff a * d = c * b.

Русский

Пусть G — коммутативная группа. Для любых a, b, c, d верно a / b = c / d ⇔ a · d = c · b.

LaTeX

$$$\\dfrac{a}{b} = \\dfrac{c}{d} \\iff a \\cdot d = c \\cdot b$$$

Lean4

@[to_additive]
theorem div_eq_div_iff_mul_eq_mul : a / b = c / d ↔ a * d = c * b :=
  by
  rw [div_eq_iff_eq_mul, div_mul_eq_mul_div, eq_comm, div_eq_iff_eq_mul']
  simp only [mul_comm, eq_comm]

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