Units in semirings and rings #
Each element of the group of units of a ring has an additive inverse.
@[simp]
Representing an element of a ring's unit group as an element of the ring commutes with mapping this element to its additive inverse.
Equations
@[simp]