Mathlib.Algebra.Group.WithOne.Units

source

0

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

Algebra.GroupWithZero.Units.Basic

Algebra.Order.Field.Defs

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