Invertible elements #
This file defines a typeclass invertible a
for elements a
with a two-sided
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
.
For constructions of the invertible element given a characteristic, see
algebra/char_p/invertible
and other lemmas in that file.
Notation #
⅟a
isinvertible.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.
Since invertible a
is not a Prop
(but it is a subsingleton
), we have to be careful about
coherence issues: we should avoid having multiple non-defeq instances for invertible a
in the
same context. This file plays it safe and uses def
rather than instance
for most definitions,
users can choose which instances to use at the point of use.
For example, here's how you can use an invertible 1
instance:
variables {α : Type*} [monoid α]
def something_that_needs_inverses (x : α) [invertible x] := sorry
section
local attribute [instance] invertible_one
def something_one := something_that_needs_inverses 1
end
Tags #
invertible, inverse element, inv_of, a half, one half, a third, one third, ½, ⅓
invertible a
gives a two-sided multiplicative inverse of a
.
Instances of this typeclass
- invertible_inv_of
- invertible_pow
- invertible.star
- matrix.invertible_transpose
- invertible_of_pos
- invertible_succ
- invertible_two
- invertible_three
- nat.arithmetic_function.zeta.invertible
- lie_algebra.orthogonal.invertible_PD
- lie_algebra.orthogonal.invertible_PB
- sym_alg.sym.invertible
- mv_polynomial.invertible_C
- mv_polynomial.invertible_coe_nat
- laurent_polynomial.invertible_T
- LDL.invertible_lower_inv
- char_zero.fintype.card.invertible
Instances of other typeclasses for invertible
- invertible.has_sizeof_inst
- invertible.subsingleton
If r
is invertible and s = r
, then s
is invertible.
Equations
- hr.copy s hs = {inv_of := ⅟ r hr, inv_of_mul_self := _, mul_inv_of_self := _}
An invertible
element is a unit.
Units are invertible in their associated monoid.
Equations
- u.invertible = {inv_of := ↑u⁻¹, inv_of_mul_self := _, mul_inv_of_self := _}
Convert is_unit
to invertible
using classical.choice
.
Prefer casesI h.nonempty_invertible
over letI := h.invertible
if you want to avoid choice.
Equations
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 variant of ring.inverse_unit
.
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 := _}