Zulip Chat Archive

Stream: Is there code for X?

Topic: is_unit_group


Kenny Lau (Jul 09 2020 at 07:28):

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 (Jul 09 2020 at 07:28):

an element of a group is a unit

Mario Carneiro (Jul 09 2020 at 08:07):

This also induces a group isomorphism between G and units G

Yury G. Kudryashov (Jul 09 2020 at 10:27):

We have this isomorphism, see to_units


Last updated: Dec 20 2023 at 11:08 UTC