Invertible elements
This file defines a typeclass invertible a for elements a with a
multiplicative inverse.
The intent of the typeclass is to provide a way to write e.g. ⅟2 in a ring
like ℤ[1/2] where some inverses exist but there is no general ⁻¹ operator;
or to specify that a field has characteristic ≠ 2.
It is the Type-valued analogue to the Prop-valued is_unit.
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.
Notation
⅟aisinvertible.inv_of a, the inverse ofa
Implementation notes
The invertible class lives in Type, not Prop, to make computation easier.
If multiplication is associative, invertible is a subsingleton anyway.
The simp normal form tries to normalize ⅟a to a ⁻¹. Otherwise, it pushes
⅟ inside the expression as much as possible.
Tags
invertible, inverse element, inv_of, a half, one half, a third, one third, ½, ⅓
invertible a gives a two-sided multiplicative inverse of a.
An invertible element is a unit.
Each element of a group is invertible.
Equations
- invertible_of_group a = {inv_of := a⁻¹, inv_of_mul_self := _, mul_inv_of_self := _}
1 is the inverse of itself
Equations
- invertible_one = {inv_of := 1, inv_of_mul_self := _, mul_inv_of_self := _}
-⅟a is the inverse of -a
Equations
- invertible_neg a = {inv_of := -⅟ a, inv_of_mul_self := _, mul_inv_of_self := _}
a is the inverse of ⅟a.
Equations
- invertible_inv_of = {inv_of := a, inv_of_mul_self := _, mul_inv_of_self := _}
⅟b * ⅟a is the inverse of a * b
Equations
- invertible_mul a b = {inv_of := ⅟ b * ⅟ a, inv_of_mul_self := _, mul_inv_of_self := _}
a⁻¹ is an inverse of a if a ≠ 0
Equations
- invertible_of_nonzero h = {inv_of := a⁻¹, inv_of_mul_self := _, mul_inv_of_self := _}
b / a is the inverse of a / b
Equations
- invertible_div a b = {inv_of := b / a, inv_of_mul_self := _, mul_inv_of_self := _}
a is the inverse of a⁻¹
Equations
- invertible_inv = {inv_of := a, inv_of_mul_self := _, mul_inv_of_self := _}
Monoid homs preserve invertibility.
Equations
- invertible.map f r = {inv_of := ⇑f (⅟ r), inv_of_mul_self := _, mul_inv_of_self := _}
A natural number t is invertible in a field K if the charactistic of K does not divide t.
Equations
A natural number t is invertible in a field K of charactistic p if p does not divide t.
Equations
Equations
A few invertible n instances for small numerals n. Feel free to add your own
number when you need its inverse.
Equations
- invertible_two = invertible_of_nonzero invertible_two._proof_1
Equations
- invertible_three = invertible_of_nonzero invertible_three._proof_1