subsingleton — Mathlib

English

For a fixed element a in a Monoid α, the inverse structure on a is unique: any two inverses of a coincide.

Русский

Для фиксированного элемента a в моноиде существует единственность обратной структуры: любые два обратных к a совпадают.

LaTeX

$$$\\forall \\alpha\\ (Monoid\\ \\alpha),\\forall a\\in\\alpha,\\forall b,c\\in\\alpha,\\ (a b = 1\\land b a = 1\\land a c = 1\\land c a = 1)\\Rightarrow b=c$$$

Lean4

instance subsingleton [Monoid α] (a : α) : Subsingleton (Invertible a) :=
  ⟨fun ⟨b, hba, hab⟩ ⟨c, _, hac⟩ => by
    congr
    exact left_inv_eq_right_inv hba hac⟩

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