# mathlibdocumentation

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 is_unit.

For constructions of the invertible element given a characteristic, see algebra/char_p/invertible and other lemmas in that file.

## 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 α] (a : α) :
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] (hac : a * b = 1) :
a = b
theorem inv_of_eq_left_inv {α : Type u} [monoid α] {a b : α} [invertible a] (hac : b * a = 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 invertible.copy {α : Type u} [monoid α] {r : α} (hr : invertible r) (s : α) (hs : s = r) :

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

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

An invertible element is a unit.

Equations
@[simp]
theorem coe_inv_unit_of_invertible {α : Type u} [monoid α] (a : α) [invertible a] :
= a
theorem is_unit_of_invertible {α : Type u} [monoid α] (a : α) [invertible a] :
def units.invertible {α : Type u} [monoid α] (u : units α) :

Units are invertible in their associated monoid.

Equations
@[simp]
theorem inv_of_units {α : Type u} [monoid α] (u : units α) [invertible u] :
theorem is_unit.nonempty_invertible {α : Type u} [monoid α] {a : α} (h : is_unit a) :
def is_unit.invertible {α : Type u} [monoid α] {a : α} (h : is_unit a) :

Convert is_unit 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_is_unit {α : Type u} [monoid α] (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
@[simp]
theorem one_sub_inv_of_two {α : Type u} [ring α] [invertible 2] :
1 - 2 = 2
@[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
theorem commute.inv_of_right {α : Type u} [monoid α] {a b : α} [invertible b] (h : b) :
( b)
theorem commute.inv_of_left {α : Type u} [monoid α] {a b : α} [invertible b] (h : a) :
commute ( b) a
theorem commute_inv_of {M : Type u_1} [has_one M] [has_mul M] (m : M) [invertible m] :
( m)
theorem nonzero_of_invertible {α : Type u} (a : α) [invertible a] :
a 0
def invertible_of_nonzero {α : Type u} {a : α} (h : 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