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/CharP/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:

variable {α : Type*} [Monoid α]

def something_that_needs_inverses (x : α) [Invertible x] := sorry

section
attribute [local instance] invertibleOne
def something_one := something_that_needs_inverses 1
end

Typeclass search vs. unification for simp lemmas

Note that since typeclass search searches the local context first, an instance argument like [Invertible a] might sometimes be filled by a different term than the one we'd find by unification (i.e., the one that's used as an implicit argument to ⅟).

This can cause issues with simp. Therefore, some lemmas are duplicated, with the @[simp] versions using unification and the user-facing ones using typeclass search.

Since unification can make backwards rewriting (e.g. rw [← mylemma]) impractical, we still want the instance-argument versions; therefore the user-facing versions retain the instance arguments and the original lemma name, whereas the @[simp]/unification ones acquire a ' at the end of their name.

We modify this file according to the above pattern only as needed; therefore, most @[simp] lemmas here are not part of such a duplicate pair. This is not (yet) intended as a permanent solution.

See Zulip: [https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Invertible.201.20simps/near/320558233]

Tags

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

class Invertible {α : Type u} [Mul α] [One α] (a : α) : Type u

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

• invOf : α

  The inverse of an Invertible element

• invOf_mul_self : ⅟a * a = 1

  invOf a is a left inverse of a

• mul_invOf_self : a * ⅟a = 1

  invOf a is a right inverse of a

theorem Invertible.invOf_mul_self {α : Type u} : ∀ {inst : Mul α} {inst_1 : One α} {a : α} [self : Invertible a], ⅟a * a = 1

invOf a is a left inverse of a

theorem Invertible.mul_invOf_self {α : Type u} : ∀ {inst : Mul α} {inst_1 : One α} {a : α} [self : Invertible a], a * ⅟a = 1

invOf a is a right inverse of a

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} [Mul α] [One α] (a : α) : ∀ {x : Invertible a}, ⅟a * a = 1

theorem invOf_mul_self {α : Type u} [Mul α] [One α] (a : α) [Invertible a] : ⅟a * a = 1

@[simp]

theorem mul_invOf_self' {α : Type u} [Mul α] [One α] (a : α) : ∀ {x : Invertible a}, a * ⅟a = 1

theorem mul_invOf_self {α : Type u} [Mul α] [One α] (a : α) [Invertible a] : a * ⅟a = 1

@[simp]

theorem invOf_mul_cancel_left' {α : Type u} [Monoid α] (a : α) (b : α) : ∀ {x : Invertible a}, ⅟a * (a * b) = b

theorem invOf_mul_cancel_left {α : Type u} [Monoid α] (a : α) (b : α) [Invertible a] : ⅟a * (a * b) = b

@[deprecated invOf_mul_cancel_left']

theorem invOf_mul_self_assoc' {α : Type u} [Monoid α] (a : α) (b : α) : ∀ {x : Invertible a}, ⅟a * (a * b) = b

Alias of invOf_mul_cancel_left'.

@[deprecated invOf_mul_cancel_left]

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

Alias of invOf_mul_cancel_left.

@[simp]

theorem mul_invOf_cancel_left' {α : Type u} [Monoid α] (a : α) (b : α) : ∀ {x : Invertible a}, a * (⅟a * b) = b

theorem mul_invOf_cancel_left {α : Type u} [Monoid α] (a : α) (b : α) [Invertible a] : a * (⅟a * b) = b

@[deprecated mul_invOf_cancel_left']

theorem mul_invOf_self_assoc' {α : Type u} [Monoid α] (a : α) (b : α) : ∀ {x : Invertible a}, a * (⅟a * b) = b

Alias of mul_invOf_cancel_left'.

@[deprecated mul_invOf_cancel_left]

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

Alias of mul_invOf_cancel_left.

@[simp]

theorem invOf_mul_cancel_right' {α : Type u} [Monoid α] (a : α) (b : α) : ∀ {x : Invertible b}, a * ⅟b * b = a

theorem invOf_mul_cancel_right {α : Type u} [Monoid α] (a : α) (b : α) [Invertible b] : a * ⅟b * b = a

@[deprecated invOf_mul_cancel_right']

theorem mul_invOf_mul_self_cancel' {α : Type u} [Monoid α] (a : α) (b : α) : ∀ {x : Invertible b}, a * ⅟b * b = a

Alias of invOf_mul_cancel_right'.

@[deprecated invOf_mul_cancel_right]

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

Alias of invOf_mul_cancel_right.

@[simp]

theorem mul_invOf_cancel_right' {α : Type u} [Monoid α] (a : α) (b : α) : ∀ {x : Invertible b}, a * b * ⅟b = a

theorem mul_invOf_cancel_right {α : Type u} [Monoid α] (a : α) (b : α) [Invertible b] : a * b * ⅟b = a

@[deprecated mul_invOf_cancel_right']

theorem mul_mul_invOf_self_cancel' {α : Type u} [Monoid α] (a : α) (b : α) : ∀ {x : Invertible b}, a * b * ⅟b = a

Alias of mul_invOf_cancel_right'.

@[deprecated mul_invOf_cancel_right]

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

Alias of mul_invOf_cancel_right.

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

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

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

instance Invertible.subsingleton {α : Type u} [Monoid α] (a : α) : Subsingleton (Invertible a)

Equations

• ⋯ = ⋯

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

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

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

If r is invertible and s = r and si = ⅟r, then s is invertible with ⅟s = si.

Equations

• hr.copy' s si hs hsi = { invOf := si, invOf_mul_self := ⋯, mul_invOf_self := ⋯ }

@[reducible, inline]

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

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

Equations

• hr.copy s hs = hr.copy' s (⅟r) hs ⋯

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

Each element of a group is invertible.

Equations

• invertibleOfGroup a = { invOf := a⁻¹, invOf_mul_self := ⋯, mul_invOf_self := ⋯ }

@[simp]

theorem invOf_eq_group_inv {α : Type u} [Group α] (a : α) [Invertible a] : ⅟a = a⁻¹

def invertibleOne {α : Type u} [Monoid α] : Invertible 1

1 is the inverse of itself

Equations

• invertibleOne = { invOf := 1, invOf_mul_self := ⋯, mul_invOf_self := ⋯ }

@[simp]

theorem invOf_one' {α : Type u} [Monoid α] : ∀ {x : Invertible 1}, ⅟1 = 1

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

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

a is the inverse of ⅟a.

Equations

• invertibleInvOf = { invOf := a, invOf_mul_self := ⋯, mul_invOf_self := ⋯ }

@[simp]

theorem invOf_invOf {α : Type u} [Monoid α] (a : α) [Invertible a] [Invertible ⅟a] : ⅟⅟a = a

@[simp]

theorem invOf_inj {α : Type u} [Monoid α] {a : α} {b : α} [Invertible a] [Invertible b] : ⅟a = ⅟b ↔ a = b

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

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

Equations

• invertibleMul a b = { invOf := ⅟b * ⅟a, invOf_mul_self := ⋯, mul_invOf_self := ⋯ }

@[simp]

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

@[reducible, inline]

abbrev Invertible.mul {α : Type u} [Monoid α] {a : α} {b : α} : Invertible a → Invertible b → Invertible (a * b)

A copy of invertibleMul for dot notation.

Equations

• x✝.mul x = invertibleMul a b

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

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

theorem invOf_mul_eq_iff_eq_mul_left {α : Type u} [Monoid α] {a : α} {b : α} {c : α} [Invertible c] : ⅟c * a = b ↔ a = c * b

theorem mul_left_eq_iff_eq_invOf_mul {α : Type u} [Monoid α] {a : α} {b : α} {c : α} [Invertible c] : c * a = b ↔ a = ⅟c * b

theorem mul_invOf_eq_iff_eq_mul_right {α : Type u} [Monoid α] {a : α} {b : α} {c : α} [Invertible c] : a * ⅟c = b ↔ a = b * c

theorem mul_right_eq_iff_eq_mul_invOf {α : Type u} [Monoid α] {a : α} {b : α} {c : α} [Invertible c] : a * c = b ↔ a = b * ⅟c