# mathlibdocumentation

algebra.invertible

# 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

• ⅟a is invertible.inv_of 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.

## Tags

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

@[class]
structure invertible {α : Type u} [has_mul α] [has_one α] :
α → Type u
• inv_of : α
• inv_of_mul_self : ( a) * a = 1
• mul_inv_of_self : a * a = 1

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

Instances
@[simp]
theorem inv_of_mul_self {α : Type u} [has_mul α] [has_one α] (a : α) [invertible a] :
( a) * a = 1

@[simp]
theorem mul_inv_of_self {α : Type u} [has_mul α] [has_one α] (a : α) [invertible a] :
a * a = 1

@[simp]
theorem inv_of_mul_self_assoc {α : Type u} [monoid α] (a b : α) [invertible a] :
( a) * a * b = b

@[simp]
theorem mul_inv_of_self_assoc {α : Type u} [monoid α] (a b : α) [invertible a] :
a * ( a) * b = b

@[simp]
theorem mul_inv_of_mul_self_cancel {α : Type u} [monoid α] (a b : α) [invertible b] :
(a * b) * b = a

@[simp]
theorem mul_mul_inv_of_self_cancel {α : Type u} [monoid α] (a b : α) [invertible b] :
(a * b) * b = a

theorem inv_of_eq_right_inv {α : Type u} [monoid α] {a b : α} [invertible a] :
a * b = 1 a = b

theorem invertible_unique {α : Type u} [monoid α] (a b : α) (h : a = b) [invertible a] [invertible b] :
a = b

@[instance]
def invertible.subsingleton {α : Type u} [monoid α] (a : α) :

def unit_of_invertible {α : Type u} [monoid α] (a : α) [invertible a] :

An invertible element is a unit.

Equations
@[simp]
theorem unit_of_invertible_val {α : Type u} [monoid α] (a : α) [invertible a] :
= a

@[simp]
theorem unit_of_invertible_inv {α : Type u} [monoid α] (a : α) [invertible a] :
= a

theorem is_unit_of_invertible {α : Type u} [monoid α] (a : α) [invertible a] :

def invertible_of_group {α : Type u} [group α] (a : α) :

Each element of a group is invertible.

Equations
@[simp]
theorem inv_of_eq_group_inv {α : Type u} [group α] (a : α) [invertible a] :

def invertible_one {α : Type u} [monoid α] :

1 is the inverse of itself

Equations
@[simp]
theorem inv_of_one {α : Type u} [monoid α] [invertible 1] :
1 = 1

def invertible_neg {α : Type u} [ring α] (a : α) [invertible a] :

-⅟a is the inverse of -a

Equations
@[simp]
theorem inv_of_neg {α : Type u} [ring α] (a : α) [invertible a] [invertible (-a)] :
(-a) = - a

@[instance]
def invertible_inv_of {α : Type u} [has_one α] [has_mul α] {a : α} [invertible a] :

a is the inverse of ⅟a.

Equations
@[simp]
theorem inv_of_inv_of {α : Type u} [monoid α] {a : α} [invertible a] [invertible ( a)] :
( a) = a

def invertible_mul {α : Type u} [monoid α] (a b : α) [invertible a] [invertible b] :

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

Equations
@[simp]
theorem inv_of_mul {α : Type u} [monoid α] (a b : α) [invertible a] [invertible b] [invertible (a * b)] :
(a * b) = ( b) * a

def invertible.copy {α : Type u} [monoid α] {r : α} (hr : invertible r) (s : α) :
s = r

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

Equations
theorem commute_inv_of {M : Type u_1} [has_one M] [has_mul M] (m : M) [invertible m] :
( m)

@[instance]
def invertible_pow {M : Type u_1} [monoid M] (m : M) [invertible m] (n : ) :

Equations
theorem nonzero_of_invertible {α : Type u} (a : α) [invertible a] :
a 0

def invertible_of_nonzero {α : Type u} {a : α} :
a 0

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

Equations
@[simp]
theorem inv_of_eq_inv {α : Type u} (a : α) [invertible a] :

@[simp]
theorem inv_mul_cancel_of_invertible {α : Type u} (a : α) [invertible a] :
a⁻¹ * a = 1

@[simp]
theorem mul_inv_cancel_of_invertible {α : Type u} (a : α) [invertible a] :
a * a⁻¹ = 1

@[simp]
theorem div_mul_cancel_of_invertible {α : Type u} (a b : α) [invertible b] :
(a / b) * b = a

@[simp]
theorem mul_div_cancel_of_invertible {α : Type u} (a b : α) [invertible b] :
a * b / b = a

@[simp]
theorem div_self_of_invertible {α : Type u} (a : α) [invertible a] :
a / a = 1

def invertible_div {α : Type u} (a b : α) [invertible a] [invertible b] :

b / a is the inverse of a / b

Equations
@[simp]
theorem inv_of_div {α : Type u} (a b : α) [invertible a] [invertible b] [invertible (a / b)] :
(a / b) = b / a

def invertible_inv {α : Type u} {a : α} [invertible a] :

a is the inverse of a⁻¹

Equations
def invertible.map {R : Type u_1} {S : Type u_2} [monoid R] [monoid S] (f : R →* S) (r : R) [invertible r] :

Monoid homs preserve invertibility.

Equations
def invertible_of_ring_char_not_dvd {K : Type u_1} [field K] {t : } :
¬ t

A natural number t is invertible in a field K if the charactistic of K does not divide t.

Equations
def invertible_of_char_p_not_dvd {K : Type u_1} [field K] {p : } [ p] {t : } :
¬p t

A natural number t is invertible in a field K of charactistic p if p does not divide t.

Equations
@[instance]
def invertible_of_pos {K : Type u_1} [field K] [char_zero K] (n : ) [h : fact (0 < n)] :

Equations
@[instance]
def invertible_succ {α : Type u} [char_zero α] (n : ) :

Equations

A few invertible n instances for small numerals n. Feel free to add your own number when you need its inverse.

@[instance]
def invertible_two {α : Type u} [char_zero α] :

Equations
@[instance]
def invertible_three {α : Type u} [char_zero α] :

Equations