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

def «term⅟_» :

Lean.ParserDescr

The inverse of an Invertible element

Equations

«term⅟_» = Lean.ParserDescr.node `term⅟_ 1024 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "⅟") (Lean.ParserDescr.cat `term 1024))

@[simp]

theorem invOf_mul_self {α : Type u} [inst : Mul α] [inst : One α] (a : α) [inst : Invertible a] :

⅟a * a = 1

@[simp]

theorem mul_invOf_self {α : Type u} [inst : Mul α] [inst : One α] (a : α) [inst : Invertible a] :

a * ⅟a = 1

@[simp]

theorem invOf_mul_self_assoc {α : Type u} [inst : Monoid α] (a : α) (b : α) [inst : Invertible a] :

⅟a * (a * b) = b

@[simp]

theorem mul_invOf_self_assoc {α : Type u} [inst : Monoid α] (a : α) (b : α) [inst : Invertible a] :

a * (⅟a * b) = b

@[simp]

theorem mul_invOf_mul_self_cancel {α : Type u} [inst : Monoid α] (a : α) (b : α) [inst : Invertible b] :

a * ⅟b * b = a

@[simp]

theorem mul_mul_invOf_self_cancel {α : Type u} [inst : Monoid α] (a : α) (b : α) [inst : Invertible b] :

a * b * ⅟b = a

theorem invOf_eq_right_inv {α : Type u} [inst : Monoid α] {a : α} {b : α} [inst : Invertible a] (hac : a * b = 1) :

⅟a = b

theorem invOf_eq_left_inv {α : Type u} [inst : Monoid α] {a : α} {b : α} [inst : Invertible a] (hac : b * a = 1) :

⅟a = b

theorem invertible_unique {α : Type u} [inst : Monoid α] (a : α) (b : α) [inst : Invertible a] [inst : Invertible b] (h : a = b) :

instance instSubsingletonInvertibleToMulToMulOneClassToOne {α : Type u} [inst : Monoid α] (a : α) :

Subsingleton (Invertible a)

Equations

@instSubsingletonInvertibleToMulToMulOneClassToOne = @instSubsingletonInvertibleToMulToMulOneClassToOne.proof_1

def Invertible.copy {α : Type u} [inst : MulOneClass α] {r : α} (hr : Invertible r) (s : α) (hs : s = r) :

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

Equations

Invertible.copy hr s hs = { invOf := ⅟r, invOf_mul_self := (_ : ⅟r * s = 1), mul_invOf_self := (_ : s * ⅟r = 1) }

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

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

@[simp]

theorem unitOfInvertible_inv {α : Type u} [inst : Monoid α] (a : α) [inst : Invertible a] :

(unitOfInvertible a).inv = ⅟a

@[simp]

theorem unitOfInvertible_val {α : Type u} [inst : Monoid α] (a : α) [inst : Invertible a] :

↑(unitOfInvertible a) = a

def unitOfInvertible {α : Type u} [inst : Monoid α] (a : α) [inst : Invertible a] :

αˣ

An invertible element is a unit.

Equations

unitOfInvertible a = { val := a, inv := ⅟a, val_inv := (_ : a * ⅟a = 1), inv_val := (_ : ⅟a * a = 1) }

theorem isUnit_of_invertible {α : Type u} [inst : Monoid α] (a : α) [inst : Invertible a] :

def Units.invertible {α : Type u} [inst : Monoid α] (u : αˣ) :

Invertible ↑u

Units are invertible in their associated monoid.

Equations

Units.invertible u = { invOf := ↑u⁻¹, invOf_mul_self := (_ : ↑u⁻¹ * ↑u = 1), mul_invOf_self := (_ : ↑u * ↑u⁻¹ = 1) }

@[simp]

theorem invOf_units {α : Type u} [inst : Monoid α] (u : αˣ) [inst : Invertible ↑u] :

⅟↑u = ↑u⁻¹

theorem IsUnit.nonempty_invertible {α : Type u} [inst : Monoid α] {a : α} (h : IsUnit a) :

Nonempty (Invertible a)

noncomputable def IsUnit.invertible {α : Type u} [inst : Monoid α] {a : α} (h : IsUnit a) :

Convert IsUnit to Invertible using Classical.choice.

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

Equations

IsUnit.invertible h = Classical.choice (_ : Nonempty (Invertible a))

@[simp]

theorem nonempty_invertible_iff_isUnit {α : Type u} [inst : Monoid α] (a : α) :

Nonempty (Invertible a) ↔ IsUnit a

def invertibleOfGroup {α : Type u} [inst : Group α] (a : α) :

Each element of a group is invertible.

Equations

invertibleOfGroup a = { invOf := a⁻¹, invOf_mul_self := (_ : a⁻¹ * a = 1), mul_invOf_self := (_ : a * a⁻¹ = 1) }

@[simp]

theorem invOf_eq_group_inv {α : Type u} [inst : Group α] (a : α) [inst : Invertible a] :

def invertibleOne {α : Type u} [inst : Monoid α] :

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 : Monoid α] :

∀ {x : Invertible 1}, ⅟1 = 1

theorem invOf_one {α : Type u} [inst : Monoid α] [inst : Invertible 1] :

⅟1 = 1

def invertibleNeg {α : Type u} [inst : Mul α] [inst : One α] [inst : HasDistribNeg α] (a : α) [inst : Invertible a] :

Invertible (-a)

-⅟a is the inverse of -a

Equations

invertibleNeg a = { invOf := -⅟a, invOf_mul_self := (_ : -⅟a * -a = 1), mul_invOf_self := (_ : -a * -⅟a = 1) }

@[simp]

theorem invOf_neg {α : Type u} [inst : Monoid α] [inst : HasDistribNeg α] (a : α) [inst : Invertible a] [inst : Invertible (-a)] :

⅟(-a) = -⅟a

@[simp]

theorem one_sub_invOf_two {α : Type u} [inst : Ring α] [inst : Invertible 2] :

1 - ⅟2 = ⅟2

@[simp]

theorem invOf_two_add_invOf_two {α : Type u} [inst : NonAssocSemiring α] [inst : Invertible 2] :

⅟2 + ⅟2 = 1

instance invertibleInvOf {α : Type u} [inst : One α] [inst : Mul α] {a : α} [inst : Invertible a] :

Invertible ⅟a

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 : Monoid α] (a : α) [inst : Invertible a] [inst : Invertible ⅟a] :

@[simp]

theorem invOf_inj {α : Type u} [inst : Monoid α] {a : α} {b : α} [inst : Invertible a] [inst : Invertible b] :

⅟a = ⅟b ↔ a = b

def invertibleMul {α : Type u} [inst : Monoid α] (a : α) (b : α) [inst : Invertible a] [inst : Invertible b] :

Invertible (a * b)

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

Equations

invertibleMul a b = { invOf := ⅟b * ⅟a, invOf_mul_self := (_ : ⅟b * ⅟a * (a * b) = 1), mul_invOf_self := (_ : a * b * (⅟b * ⅟a) = 1) }

@[simp]

theorem invOf_mul {α : Type u} [inst : Monoid α] (a : α) (b : α) [inst : Invertible a] [inst : Invertible b] [inst : Invertible (a * b)] :

⅟(a * b) = ⅟b * ⅟a

theorem mul_right_inj_of_invertible {α : Type u} {a : α} {b : α} [inst : Monoid α] (c : α) [inst : Invertible c] :

a * c = b * c ↔ a = b

theorem mul_left_inj_of_invertible {α : Type u} {a : α} {b : α} [inst : Monoid α] (c : α) [inst : Invertible c] :

c * a = c * b ↔ a = b

theorem invOf_mul_eq_iff_eq_mul_left {α : Type u} {c : α} {a : α} {b : α} [inst : Monoid α] [inst : Invertible c] :

⅟c * a = b ↔ a = c * b

theorem mul_left_eq_iff_eq_invOf_mul {α : Type u} {c : α} {a : α} {b : α} [inst : Monoid α] [inst : Invertible c] :

c * a = b ↔ a = ⅟c * b

theorem mul_invOf_eq_iff_eq_mul_right {α : Type u} {c : α} {a : α} {b : α} [inst : Monoid α] [inst : Invertible c] :

a * ⅟c = b ↔ a = b * c

theorem mul_right_eq_iff_eq_mul_invOf {α : Type u} {c : α} {a : α} {b : α} [inst : Monoid α] [inst : Invertible c] :

a * c = b ↔ a = b * ⅟c

theorem Commute.invOf_right {α : Type u} [inst : Monoid α] {a : α} {b : α} [inst : Invertible b] (h : Commute a b) :

theorem Commute.invOf_left {α : Type u} [inst : Monoid α] {a : α} {b : α} [inst : Invertible b] (h : Commute b a) :

Commute (⅟b) a

theorem commute_invOf {M : Type u_1} [inst : One M] [inst : Mul M] (m : M) [inst : Invertible m] :

theorem nonzero_of_invertible {α : Type u} [inst : MulZeroOneClass α] (a : α) [inst : Nontrivial α] [inst : Invertible a] :

a ≠ 0

theorem pos_of_invertible_cast {α : Type u} [inst : Semiring α] [inst : Nontrivial α] (n : ℕ) [inst : Invertible ↑n] :

0 < n

instance Invertible.ne_zero {α : Type u} [inst : MulZeroOneClass α] [inst : Nontrivial α] (a : α) [inst : Invertible a] :

Equations

@Invertible.ne_zero = @Invertible.ne_zero.proof_1

@[simp]

theorem Ring.inverse_invertible {α : Type u} [inst : MonoidWithZero α] (x : α) [inst : Invertible x] :

Ring.inverse x = ⅟x

A variant of Ring.inverse_unit.

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

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

Equations

invertibleOfNonzero h = { invOf := a⁻¹, invOf_mul_self := (_ : a⁻¹ * a = 1), mul_invOf_self := (_ : a * a⁻¹ = 1) }

@[simp]

theorem invOf_eq_inv {α : Type u} [inst : GroupWithZero α] (a : α) [inst : Invertible a] :

@[simp]

theorem inv_mul_cancel_of_invertible {α : Type u} [inst : GroupWithZero α] (a : α) [inst : Invertible a] :

a⁻¹ * a = 1

@[simp]

theorem mul_inv_cancel_of_invertible {α : Type u} [inst : GroupWithZero α] (a : α) [inst : Invertible a] :

a * a⁻¹ = 1

@[simp]

theorem div_mul_cancel_of_invertible {α : Type u} [inst : GroupWithZero α] (a : α) (b : α) [inst : Invertible b] :

a / b * b = a

@[simp]

theorem mul_div_cancel_of_invertible {α : Type u} [inst : GroupWithZero α] (a : α) (b : α) [inst : Invertible b] :

a * b / b = a

@[simp]

theorem div_self_of_invertible {α : Type u} [inst : GroupWithZero α] (a : α) [inst : Invertible a] :

a / a = 1

def invertibleDiv {α : Type u} [inst : GroupWithZero α] (a : α) (b : α) [inst : Invertible a] [inst : Invertible b] :

Invertible (a / b)

b / a is the inverse of a / b

Equations

invertibleDiv a b = { 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 : GroupWithZero α] (a : α) (b : α) [inst : Invertible a] [inst : Invertible b] [inst : Invertible (a / b)] :

⅟(a / b) = b / a

def invertibleInv {α : Type u} [inst : GroupWithZero α] {a : α} [inst : Invertible a] :

Invertible a⁻¹

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 : MulOneClass R] [inst : MulOneClass S] [inst : MonoidHomClass F R S] (f : F) (r : R) [inst : Invertible r] :

Invertible (↑f r)

Monoid homs preserve invertibility.

Equations

Invertible.map f r = { 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 : MulOneClass R] [inst : Monoid S] [inst : MonoidHomClass F R S] (f : F) (r : R) [inst : Invertible r] [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 : MulOneClass R] [inst : MulOneClass S] [inst : MonoidHomClass G S R] (f : R → S) (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 : MulOneClass R] [inst : MulOneClass S] [inst : MonoidHomClass G S R] (f : R → S) (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

Invertible.ofLeftInverse f g r h = Invertible.copy (Invertible.map g (f r)) r (_ : r = ↑g (f r))

@[simp]

theorem invertibleEquivOfLeftInverse_apply {R : Type u_1} {S : Type u_2} {F : Type u_3} {G : Type u_4} [inst : Monoid R] [inst : Monoid S] [inst : MonoidHomClass F R S] [inst : MonoidHomClass G S R] (f : F) (g : G) (r : R) (h : Function.LeftInverse ↑g ↑f) :

∀ (x : Invertible (↑f r)), ↑(invertibleEquivOfLeftInverse f g r h) 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 : Monoid R] [inst : Monoid S] [inst : MonoidHomClass F R S] [inst : MonoidHomClass G S R] (f : F) (g : G) (r : R) (h : Function.LeftInverse ↑g ↑f) :

∀ (x : Invertible r), ↑(Equiv.symm (invertibleEquivOfLeftInverse f g r h)) x = Invertible.map f r

def invertibleEquivOfLeftInverse {R : Type u_1} {S : Type u_2} {F : Type u_3} {G : Type u_4} [inst : Monoid R] [inst : Monoid S] [inst : MonoidHomClass F R S] [inst : MonoidHomClass G S R] (f : F) (g : G) (r : R) (h : Function.LeftInverse ↑g ↑f) :

Invertible (↑f r) ≃ Invertible 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.