# Documentation

Mathlib.Algebra.Invertible

# 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 IsUnit.

For constructions of the invertible element given a characteristic, see Algebra/Char_P/Invertible and other lemmas in that file.

## Notation #

• ⅟a is Invertible.invOf a, the inverse of a

## 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] invertibleOne
def something_one := something_that_needs_inverses 1
end


## Tags #

invertible, inverse element, invOf, a half, one half, a third, one third, ½, ⅓

class Invertible {α : Type u} [inst : Mul α] [inst : One α] (a : α) :
• The inverse of an Invertible element

invOf : α
• invOf a is a left inverse of a

invOf_mul_self : invOf * a = 1
• invOf a is a right inverse of a

mul_invOf_self : a * invOf = 1

Invertible a gives a two-sided multiplicative inverse of a.

Instances

The inverse of an Invertible element

Equations
@[simp]
theorem invOf_mul_self {α : Type u} [inst : Mul α] [inst : One α] (a : α) [inst : ] :
a * a = 1
@[simp]
theorem mul_invOf_self {α : Type u} [inst : Mul α] [inst : One α] (a : α) [inst : ] :
a * a = 1
@[simp]
theorem invOf_mul_self_assoc {α : Type u} [inst : ] (a : α) (b : α) [inst : ] :
a * (a * b) = b
@[simp]
theorem mul_invOf_self_assoc {α : Type u} [inst : ] (a : α) (b : α) [inst : ] :
a * (a * b) = b
@[simp]
theorem mul_invOf_mul_self_cancel {α : Type u} [inst : ] (a : α) (b : α) [inst : ] :
a * b * b = a
@[simp]
theorem mul_mul_invOf_self_cancel {α : Type u} [inst : ] (a : α) (b : α) [inst : ] :
a * b * b = a
theorem invOf_eq_right_inv {α : Type u} [inst : ] {a : α} {b : α} [inst : ] (hac : a * b = 1) :
a = b
theorem invOf_eq_left_inv {α : Type u} [inst : ] {a : α} {b : α} [inst : ] (hac : b * a = 1) :
a = b
theorem invertible_unique {α : Type u} [inst : ] (a : α) (b : α) [inst : ] [inst : ] (h : a = b) :
instance instSubsingletonInvertibleToMulToMulOneClassToOne {α : Type u} [inst : ] (a : α) :
Equations
def Invertible.copy {α : Type u} [inst : ] {r : α} (hr : ) (s : α) (hs : s = r) :

If r is invertible and s = r, then s is invertible.

Equations
theorem Invertible.congr {α : Type u} [inst : Ring α] (a : α) (b : α) [inst : ] [inst : ] (h : a = b) :

If a is invertible and a = b, then ⅟a = ⅟b.

@[simp]
theorem unitOfInvertible_inv {α : Type u} [inst : ] (a : α) [inst : ] :
().inv = a
@[simp]
theorem unitOfInvertible_val {α : Type u} [inst : ] (a : α) [inst : ] :
↑() = a
def unitOfInvertible {α : Type u} [inst : ] (a : α) [inst : ] :
αˣ

An invertible element is a unit.

Equations
• = { val := a, inv := a, val_inv := (_ : a * a = 1), inv_val := (_ : a * a = 1) }
theorem isUnit_of_invertible {α : Type u} [inst : ] (a : α) [inst : ] :
def Units.invertible {α : Type u} [inst : ] (u : αˣ) :

Units are invertible in their associated monoid.

Equations
• = { invOf := u⁻¹, invOf_mul_self := (_ : u⁻¹ * u = 1), mul_invOf_self := (_ : u * u⁻¹ = 1) }
@[simp]
theorem invOf_units {α : Type u} [inst : ] (u : αˣ) [inst : ] :
u = u⁻¹
theorem IsUnit.nonempty_invertible {α : Type u} [inst : ] {a : α} (h : ) :
noncomputable def IsUnit.invertible {α : Type u} [inst : ] {a : α} (h : ) :

Convert IsUnit to Invertible using Classical.choice.

Prefer casesI h.nonempty_invertible over letI := h.invertible if you want to avoid choice.

Equations
@[simp]
theorem nonempty_invertible_iff_isUnit {α : Type u} [inst : ] (a : α) :
def invertibleOfGroup {α : Type u} [inst : ] (a : α) :

Each element of a group is invertible.

Equations
• = { invOf := a⁻¹, invOf_mul_self := (_ : a⁻¹ * a = 1), mul_invOf_self := (_ : a * a⁻¹ = 1) }
@[simp]
theorem invOf_eq_group_inv {α : Type u} [inst : ] (a : α) [inst : ] :
def invertibleOne {α : Type u} [inst : ] :

1 is the inverse of itself

Equations
• invertibleOne = { invOf := 1, invOf_mul_self := (_ : 1 * 1 = 1), mul_invOf_self := (_ : 1 * 1 = 1) }
@[simp]
theorem invOf_one' {α : Type u} [inst : ] :
∀ {x : }, 1 = 1
theorem invOf_one {α : Type u} [inst : ] [inst : ] :
1 = 1
def invertibleNeg {α : Type u} [inst : Mul α] [inst : One α] [inst : ] (a : α) [inst : ] :

-⅟a is the inverse of -a

Equations
• = { invOf := -a, invOf_mul_self := (_ : -a * -a = 1), mul_invOf_self := (_ : -a * -a = 1) }
@[simp]
theorem invOf_neg {α : Type u} [inst : ] [inst : ] (a : α) [inst : ] [inst : Invertible (-a)] :
(-a) = -a
@[simp]
theorem one_sub_invOf_two {α : Type u} [inst : Ring α] [inst : ] :
1 - 2 = 2
@[simp]
theorem invOf_two_add_invOf_two {α : Type u} [inst : ] [inst : ] :
2 + 2 = 1
instance invertibleInvOf {α : Type u} [inst : One α] [inst : Mul α] {a : α} [inst : ] :

a is the inverse of ⅟a.

Equations
• invertibleInvOf = { invOf := a, invOf_mul_self := (_ : a * a = 1), mul_invOf_self := (_ : a * a = 1) }
@[simp]
theorem invOf_invOf {α : Type u} [inst : ] (a : α) [inst : ] [inst : ] :
@[simp]
theorem invOf_inj {α : Type u} [inst : ] {a : α} {b : α} [inst : ] [inst : ] :
a = b a = b
def invertibleMul {α : Type u} [inst : ] (a : α) (b : α) [inst : ] [inst : ] :

⅟b * ⅟a is the inverse of a * b

Equations
@[simp]
theorem invOf_mul {α : Type u} [inst : ] (a : α) (b : α) [inst : ] [inst : ] [inst : Invertible (a * b)] :
(a * b) = b * a
theorem mul_right_inj_of_invertible {α : Type u} {a : α} {b : α} [inst : ] (c : α) [inst : ] :
a * c = b * c a = b
theorem mul_left_inj_of_invertible {α : Type u} {a : α} {b : α} [inst : ] (c : α) [inst : ] :
c * a = c * b a = b
theorem invOf_mul_eq_iff_eq_mul_left {α : Type u} {c : α} {a : α} {b : α} [inst : ] [inst : ] :
c * a = b a = c * b
theorem mul_left_eq_iff_eq_invOf_mul {α : Type u} {c : α} {a : α} {b : α} [inst : ] [inst : ] :
c * a = b a = c * b
theorem mul_invOf_eq_iff_eq_mul_right {α : Type u} {c : α} {a : α} {b : α} [inst : ] [inst : ] :
a * c = b a = b * c
theorem mul_right_eq_iff_eq_mul_invOf {α : Type u} {c : α} {a : α} {b : α} [inst : ] [inst : ] :
a * c = b a = b * c
theorem Commute.invOf_right {α : Type u} [inst : ] {a : α} {b : α} [inst : ] (h : Commute a b) :
theorem Commute.invOf_left {α : Type u} [inst : ] {a : α} {b : α} [inst : ] (h : Commute b a) :
theorem commute_invOf {M : Type u_1} [inst : One M] [inst : Mul M] (m : M) [inst : ] :
theorem nonzero_of_invertible {α : Type u} [inst : ] (a : α) [inst : ] [inst : ] :
a 0
theorem pos_of_invertible_cast {α : Type u} [inst : ] [inst : ] (n : ) [inst : ] :
0 < n
instance Invertible.ne_zero {α : Type u} [inst : ] [inst : ] (a : α) [inst : ] :
Equations
@[simp]
theorem Ring.inverse_invertible {α : Type u} [inst : ] (x : α) [inst : ] :

A variant of Ring.inverse_unit.

def invertibleOfNonzero {α : Type u} [inst : ] {a : α} (h : a 0) :

a⁻¹ is an inverse of a if a ≠ 0

Equations
• = { invOf := a⁻¹, invOf_mul_self := (_ : a⁻¹ * a = 1), mul_invOf_self := (_ : a * a⁻¹ = 1) }
@[simp]
theorem invOf_eq_inv {α : Type u} [inst : ] (a : α) [inst : ] :
@[simp]
theorem inv_mul_cancel_of_invertible {α : Type u} [inst : ] (a : α) [inst : ] :
a⁻¹ * a = 1
@[simp]
theorem mul_inv_cancel_of_invertible {α : Type u} [inst : ] (a : α) [inst : ] :
a * a⁻¹ = 1
@[simp]
theorem div_mul_cancel_of_invertible {α : Type u} [inst : ] (a : α) (b : α) [inst : ] :
a / b * b = a
@[simp]
theorem mul_div_cancel_of_invertible {α : Type u} [inst : ] (a : α) (b : α) [inst : ] :
a * b / b = a
@[simp]
theorem div_self_of_invertible {α : Type u} [inst : ] (a : α) [inst : ] :
a / a = 1
def invertibleDiv {α : Type u} [inst : ] (a : α) (b : α) [inst : ] [inst : ] :

b / a is the inverse of a / b

Equations
• = { invOf := b / a, invOf_mul_self := (_ : b / a * (a / b) = 1), mul_invOf_self := (_ : a / b * (b / a) = 1) }
theorem invOf_div {α : Type u} [inst : ] (a : α) (b : α) [inst : ] [inst : ] [inst : Invertible (a / b)] :
(a / b) = b / a
def invertibleInv {α : Type u} [inst : ] {a : α} [inst : ] :

a is the inverse of a⁻¹

Equations
• invertibleInv = { invOf := a, invOf_mul_self := (_ : a * a⁻¹ = 1), mul_invOf_self := (_ : a⁻¹ * a = 1) }
def Invertible.map {R : Type u_1} {S : Type u_2} {F : Type u_3} [inst : ] [inst : ] [inst : ] (f : F) (r : R) [inst : ] :
Invertible (f r)

Monoid homs preserve invertibility.

Equations
• = { invOf := f r, invOf_mul_self := (_ : f r * f r = 1), mul_invOf_self := (_ : f r * f r = 1) }
theorem map_invOf {R : Type u_1} {S : Type u_2} {F : Type u_3} [inst : ] [inst : ] [inst : ] (f : F) (r : R) [inst : ] [ifr : Invertible (f r)] :
f r = (f r)

Note that the invertible (f r) argument can be satisfied by using letI := invertible.map f r before applying this lemma.

theorem Invertible.ofLeftInverse_invOf {R : Type u_1} {S : Type u_2} {G : Type u_3} [inst : ] [inst : ] [inst : ] (f : RS) (g : G) (r : R) (h : Function.LeftInverse (g) f) [inst : Invertible (f r)] :
r = (g (f r))
def Invertible.ofLeftInverse {R : Type u_1} {S : Type u_2} {G : Type u_3} [inst : ] [inst : ] [inst : ] (f : RS) (g : G) (r : R) (h : Function.LeftInverse (g) f) [inst : Invertible (f r)] :

If a function f : R → S has a left-inverse that is a monoid hom, then r : R is invertible if f r is.

The inverse is computed as g (⅟(f r))

Equations
@[simp]
theorem invertibleEquivOfLeftInverse_apply {R : Type u_1} {S : Type u_2} {F : Type u_3} {G : Type u_4} [inst : ] [inst : ] [inst : ] [inst : ] (f : F) (g : G) (r : R) (h : ) :
∀ (x : Invertible (f r)), ↑() x = Invertible.ofLeftInverse (f) g r h
@[simp]
theorem invertibleEquivOfLeftInverse_symm_apply {R : Type u_1} {S : Type u_2} {F : Type u_3} {G : Type u_4} [inst : ] [inst : ] [inst : ] [inst : ] (f : F) (g : G) (r : R) (h : ) :
∀ (x : ), ↑(Equiv.symm ()) x =
def invertibleEquivOfLeftInverse {R : Type u_1} {S : Type u_2} {F : Type u_3} {G : Type u_4} [inst : ] [inst : ] [inst : ] [inst : ] (f : F) (g : G) (r : R) (h : ) :
Invertible (f r)

Invertibility on either side of a monoid hom with a left-inverse is equivalent.

Equations
• One or more equations did not get rendered due to their size.