toUniqueUnits — Mathlib

English

In a canonically ordered commutative monoid, every unit is equal to 1; equivalently, the group of units is trivial.

Русский

В канонически упорядоченном коммутативном моноиде вся единица равна единице; следовательно, группа единиц тривиальна.

LaTeX

$$$\forall u \in \mathrm{Units}(\alpha),\ u = 1$$$

Lean4

@[to_additive]
instance toUniqueUnits : Unique αˣ where uniq a := Units.ext <| le_one_iff_eq_one.mp (le_of_mul_le_left a.mul_inv.le)

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