Groups with an adjoined zero element #
This file describes structures that are not usually studied on their own right in mathematics, namely a special sort of monoid: apart from a distinguished “zero element” they form a group, or in other words, they are groups with an adjoined zero element.
- division rings;
- the value monoid of a multiplicative valuation;
- in particular, the non-negative real numbers.
Main definitions #
Implementation details #
As is usual in mathlib, we extend the inverse function to the zero element,
0⁻¹ = 0.
In a monoid with zero, if zero equals one, then zero is the unique element.
Somewhat arbitrarily, we define the default element to be
All other elements will be provably equal to it, but not necessarily definitionally equal.