Isomorphism between a group and the units of itself adjoined with 0

Notes

This is here to keep Algebra.GroupWithZero.Units.Basic out of the import requirements of Algebra.Order.Field.Defs.

def WithZero.unitsWithZeroEquiv {α : Type u_1} [Group α] : (WithZero α)ˣ ≃* α

Any group is isomorphic to the units of itself adjoined with 0.

Equations

• One or more equations did not get rendered due to their size.