English
A group G is isomorphic to its group of units Gˣ; more precisely, there exists a multiplicative equivalence φ: G ≃* Gˣ given by φ(g) = (g, g^{-1}, ...) with φ^{-1} = identity on units.
Русский
Группа G изоморфна своей группе единиц Gˣ; существует мультипликативное эквивалентное отображение φ: G ≃* Gˣ, задающееся φ(g) = (g, g^{-1}, ...).
LaTeX
$$$G \\cong G^{\\times}$$$
Lean4
/-- A group is isomorphic to its group of units. -/
@[to_additive (attr := simps apply_val symm_apply) /-- An additive group is isomorphic to its group of additive units -/
]
def toUnits [Group G] : G ≃* Gˣ
where
toFun x := ⟨x, x⁻¹, mul_inv_cancel _, inv_mul_cancel _⟩
invFun x := x
map_mul' _ _ := Units.ext rfl
