is_unit_group

Stream: Is there code for X?

[Kenny Lau]

theorem is_unit_group {G : Type v} [group G] (x : G) : is_unit x :=
⟨⟨x, x⁻¹, mul_inv_self x, inv_mul_self x⟩, rfl⟩

[Kenny Lau]

an element of a group is a unit

[Mario Carneiro]

This also induces a group isomorphism between G and units G

[Yury G. Kudryashov]

We have this isomorphism, see to_units