div_eq_div_iff_div_eq_div — Mathlib

English

For any a in G, the map x ↦ a / x is an involution on G, i.e. a / (a / x) = x for all x in G.

Русский

Для любого a ∈ G отображение x ↦ a / x является инволюцией на G, то есть a / (a / x) = x для всех x ∈ G.

LaTeX

$$$\\forall x, \\; a / (a / x) = x$$$

Lean4

@[to_additive]
theorem div_eq_div_iff_div_eq_div : a / b = c / d ↔ a / c = b / d := by
  rw [div_eq_iff_eq_mul, div_mul_eq_mul_div, div_eq_iff_eq_mul', mul_div_assoc]

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