Isomorphism between a group and the units of itself adjoined with 0 #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
Notes #
This is here to keep algebra.group_with_zero.units.basic out of the import requirements of
algebra.order.field.defs.
Any group is isomorphic to the units of itself adjoined with 0.
Equations
- with_zero.units_with_zero_equiv = {to_fun := λ (a : (with_zero α)ˣ), with_zero.unzero _, inv_fun := λ (a : α), units.mk0 ↑a with_zero.coe_ne_zero, left_inv := _, right_inv := _, map_mul' := _}