English
The units of a monoid α are in natural equivalence with the subset of α × α consisting of pairs (u, v) with u v = 1 = v u; more precisely, there is a canonical equivalence αˣ ≃ { (p: α×α) // p.1 p.2 = 1 ∧ p.2 p.1 = 1 } sending a unit u to (u, u⁻¹).
Русский
Единицы моноида α эквивалентны подтипу пар (u, v) из α×α, удовлетворяющих u v = 1 = v u; конкретно существует каноническое эквивалентное отображение αˣ ≃ { (p1, p2) | p1 p2 = 1 ∧ p2 p1 = 1 }, отправляющее элемент-единицу u в пару (u, u⁻¹).
LaTeX
$$$α^{\\times} \\;\\simeq\\; \\{ p=(p_1,p_2)\\in α\\times α\\;\\big|\\; p_1 p_2=1 \\wedge p_2 p_1=1\\}$$$
Lean4
/-- The `αˣ` type is equivalent to a subtype of `α × α`. -/
@[simps]
def unitsEquivProdSubtype [Monoid α] : αˣ ≃ { p : α × α // p.1 * p.2 = 1 ∧ p.2 * p.1 = 1 }
where
toFun u := ⟨(u, ↑u⁻¹), u.val_inv, u.inv_val⟩
invFun p := Units.mk (p : α × α).1 (p : α × α).2 p.prop.1 p.prop.2
