Lemmas about units in a
MonoidWithZero or a
Introduce a function
inverse on a monoid with zero
M₀, which sends
invertible and to
0 otherwise. This definition is somewhat ad hoc, but one needs a fully (rather
than partially) defined inverse function for some purposes, including for calculus.
Note that while this is in the
Ring namespace for brevity, it requires the weaker assumption
MonoidWithZero M₀ instead of
Embed a non-zero element of a
GroupWithZero into the unit group.
By combining this function with the operations on units,
/ₚ operation, it is possible to write a division
as a partial function with three arguments.