# Documentation

Mathlib.Algebra.Group.WithOne.Units

# 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} [inst : ] :
()ˣ ≃* α

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.