Zulip Chat Archive

Stream: Is there code for X?

Topic: is_unit_group


view this post on Zulip 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

view this post on Zulip Kenny Lau (Jul 09 2020 at 07:28):

an element of a group is a unit

view this post on Zulip Mario Carneiro (Jul 09 2020 at 08:07):

This also induces a group isomorphism between G and units G

view this post on Zulip Yury G. Kudryashov (Jul 09 2020 at 10:27):

We have this isomorphism, see to_units


Last updated: May 17 2021 at 16:26 UTC