mathlib documentation

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 α] (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 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 invertible_unique {α : Type u} [monoid α] (a b : α) (h : a = b) [invertible a] [invertible b] :

@[instance]

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

subsingleton (invertible a)

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

An invertible element is a unit.

Equations

unit_of_invertible a = {val := a, inv := ⅟ a _inst_2, val_inv := _, inv_val := _}

@[simp]

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

↑(unit_of_invertible a) = a

@[simp]

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

↑(unit_of_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

invertible_of_group a = {inv_of := a⁻¹, inv_of_mul_self := _, mul_inv_of_self := _}

@[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

invertible_one = {inv_of := 1, inv_of_mul_self := _, mul_inv_of_self := _}

@[simp]

theorem inv_of_one {α : Type u} [monoid α] [invertible 1] :

⅟ 1 = 1

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

invertible (-a)

-⅟a is the inverse of -a

Equations

invertible_neg a = {inv_of := -⅟ a, inv_of_mul_self := _, mul_inv_of_self := _}

@[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] :

invertible (⅟ a)

a is the inverse of ⅟a.

Equations

invertible_inv_of = {inv_of := a, inv_of_mul_self := _, mul_inv_of_self := _}

@[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] :

invertible (a * b)

⅟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 := _}

@[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 : α) (hs : s = r) :

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 := _}

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

commute m (⅟ m)

@[instance]

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

invertible (m ^ n)

Equations

invertible_pow m n = {inv_of := ⅟ m ^ n, inv_of_mul_self := _, mul_inv_of_self := _}

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

a ≠ 0

def invertible_of_nonzero {α : Type u} [group_with_zero α] {a : α} (h : a ≠ 0) :

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 := _}

@[simp]

theorem inv_of_eq_inv {α : Type u} [group_with_zero α] (a : α) [invertible a] :

@[simp]

theorem inv_mul_cancel_of_invertible {α : Type u} [group_with_zero α] (a : α) [invertible a] :

a⁻¹ * a = 1

@[simp]

theorem mul_inv_cancel_of_invertible {α : Type u} [group_with_zero α] (a : α) [invertible a] :

a * a⁻¹ = 1

@[simp]

theorem div_mul_cancel_of_invertible {α : Type u} [group_with_zero α] (a b : α) [invertible b] :

(a / b) * b = a

@[simp]

theorem mul_div_cancel_of_invertible {α : Type u} [group_with_zero α] (a b : α) [invertible b] :

a * b / b = a

@[simp]

theorem div_self_of_invertible {α : Type u} [group_with_zero α] (a : α) [invertible a] :

a / a = 1

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

invertible (a / b)

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 := _}

@[simp]

theorem inv_of_div {α : Type u} [group_with_zero α] (a b : α) [invertible a] [invertible b] [invertible (a / b)] :

⅟ (a / b) = b / a

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

invertible a⁻¹

a is the inverse of a⁻¹

Equations

invertible_inv = {inv_of := a, inv_of_mul_self := _, mul_inv_of_self := _}

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

invertible (⇑f r)

Monoid homs preserve invertibility.

Equations

invertible.map f r = {inv_of := ⇑f (⅟ r), inv_of_mul_self := _, mul_inv_of_self := _}

def invertible_of_ring_char_not_dvd {K : Type u_1} [field K] {t : ℕ} (not_dvd : ¬ring_char K ∣ t) :

invertible ↑t

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

Equations

invertible_of_ring_char_not_dvd not_dvd = invertible_of_nonzero _

def invertible_of_char_p_not_dvd {K : Type u_1} [field K] {p : ℕ} [char_p K p] {t : ℕ} (not_dvd : ¬p ∣ t) :

invertible ↑t

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

Equations

invertible_of_char_p_not_dvd not_dvd = invertible_of_nonzero _

@[instance]

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

invertible ↑n

Equations

invertible_of_pos n = invertible_of_nonzero _

@[instance]

def invertible_succ {α : Type u} [division_ring α] [char_zero α] (n : ℕ) :

invertible ↑(n.succ)

Equations

invertible_succ n = invertible_of_nonzero _

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} [division_ring α] [char_zero α] :

Equations

invertible_two = invertible_of_nonzero invertible_two._proof_1

@[instance]

def invertible_three {α : Type u} [division_ring α] [char_zero α] :

Equations

invertible_three = invertible_of_nonzero invertible_three._proof_1