This file defines a typeclass
invertible a for elements
a with a
The intent of the typeclass is to provide a way to write e.g.
⅟2 in a ring
ℤ[1/2] where some inverses exist but there is no general
or to specify that a field has characteristic
It is the
Type-valued analogue to the
This file also includes some instances of
invertible for specific numbers in
characteristic zero. Some more cases are given as a
def, to be included only
when needed. To construct instances for concrete numbers,
invertible_of_nonzero is a useful definition.
invertible.inv_of a, the inverse of
simp normal form tries to normalize
a ⁻¹. Otherwise, it pushes
⅟ inside the expression as much as possible.
invertible, inverse element, inv_of, a half, one half, a third, one third, ½, ⅓
invertible a gives a two-sided multiplicative inverse of
invertible n instances for small numerals
n. Feel free to add your own
number when you need its inverse.