Invertible elements #
This file defines a typeclass
invertible a for elements
a with a two-sided
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
For constructions of the invertible element given a characteristic, see
algebra/char_p/invertible and other lemmas in that file.
invertible.inv_of a, the inverse of
Implementation notes #
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