div_eq_one_iff_eq — Mathlib

English

Let α be a DivisionMonoid and let b be a unit (b ∈ α×). Then a/b = 1 if and only if a = b, for all a ∈ α.

Русский

Пусть α — делимый моноид, и пусть b является единицей (b ∈ α×). Тогда для всех a ∈ α выполняется a / b = 1 тогда и только тогда, когда a = b.

LaTeX

$$$$ \\forall a,b \\in \\alpha,\\ b \\in \\alpha^{\\times} \\implies \\frac{a}{b} = 1 \\iff a = b. $$$$

Lean4

@[to_additive]
protected theorem div_eq_one_iff_eq (h : IsUnit b) : a / b = 1 ↔ a = b :=
  ⟨eq_of_div_eq_one, fun hab => hab.symm ▸ h.div_self⟩

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