Theorems about invertible elements

@[simp]

theorem val_unitOfInvertible {α : Type u} [Monoid α] (a : α) [Invertible a] : ↑(unitOfInvertible a) = a

@[simp]

theorem val_inv_unitOfInvertible {α : Type u} [Monoid α] (a : α) [Invertible a] : ↑(unitOfInvertible a)⁻¹ = ⅟a

def unitOfInvertible {α : Type u} [Monoid α] (a : α) [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} [Monoid α] (a : α) [Invertible a] : IsUnit a

def Units.invertible {α : Type u} [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} [Monoid α] (u : αˣ) [Invertible ↑u] : ⅟↑u = ↑u⁻¹

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

noncomputable def IsUnit.invertible {α : Type u} [Monoid α] {a : α} (h : IsUnit a) : Invertible 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} [Monoid α] (a : α) : Nonempty (Invertible a) ↔ IsUnit a

def invertibleNeg {α : Type u} [Mul α] [One α] [HasDistribNeg α] (a : α) [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} [Monoid α] [HasDistribNeg α] (a : α) [Invertible a] [Invertible (-a)] : ⅟(-a) = -⅟a

@[simp]

theorem one_sub_invOf_two {α : Type u} [Ring α] [Invertible 2] : 1 - ⅟2 = ⅟2

@[simp]

theorem invOf_two_add_invOf_two {α : Type u} [NonAssocSemiring α] [Invertible 2] : ⅟2 + ⅟2 = 1

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

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

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

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

@[reducible]

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

This is the Invertible version of Units.isUnit_units_mul

Equations

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

@[reducible]

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

This is the Invertible version of Units.isUnit_mul_units

Equations

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

@[simp]

theorem Invertible.mulLeft_apply {α : Type u} [Monoid α] {a : α} : ∀ (x : Invertible a) (b : α) (x_1 : Invertible b), (Invertible.mulLeft x b) x_1 = invertibleMul a b

@[simp]

theorem Invertible.mulLeft_symm_apply {α : Type u} [Monoid α] {a : α} : ∀ (x : Invertible a) (b : α) (x_1 : Invertible (a * b)), (Invertible.mulLeft x b).symm x_1 = invertibleOfInvertibleMul a b

def Invertible.mulLeft {α : Type u} [Monoid α] {a : α} : Invertible a → (b : α) → Invertible b ≃ Invertible (a * b)

invertibleOfInvertibleMul and invertibleMul as an equivalence.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Invertible.mulRight_apply {α : Type u} [Monoid α] (a : α) {b : α} : ∀ (x : Invertible b) (x_1 : Invertible a), (Invertible.mulRight a x) x_1 = invertibleMul a b

@[simp]

theorem Invertible.mulRight_symm_apply {α : Type u} [Monoid α] (a : α) {b : α} : ∀ (x : Invertible b) (x_1 : Invertible (a * b)), (Invertible.mulRight a x).symm x_1 = invertibleOfMulInvertible a b

def Invertible.mulRight {α : Type u} [Monoid α] (a : α) {b : α} : Invertible b → Invertible a ≃ Invertible (a * b)

invertibleOfMulInvertible and invertibleMul as an equivalence.

Equations

• One or more equations did not get rendered due to their size.

instance invertiblePow {α : Type u} [Monoid α] (m : α) [Invertible m] (n : ℕ) : Invertible (m ^ n)

Equations

• invertiblePow m n = { invOf := ⅟m ^ n, invOf_mul_self := (_ : ⅟m ^ n * m ^ n = 1), mul_invOf_self := (_ : m ^ n * ⅟m ^ n = 1) }

theorem invOf_pow {α : Type u} [Monoid α] (m : α) [Invertible m] (n : ℕ) [Invertible (m ^ n)] : ⅟(m ^ n) = ⅟m ^ n

def invertibleOfPowEqOne {α : Type u} [Monoid α] (x : α) (n : ℕ) (hx : x ^ n = 1) (hn : n ≠ 0) : Invertible x

If x ^ n = 1 then x has an inverse, x^(n - 1).

Equations

• invertibleOfPowEqOne x n hx hn = Units.invertible (Units.ofPowEqOne x n hx hn)

@[simp]

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

A variant of Ring.inverse_unit.

@[simp]

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

@[simp]

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

@[simp]

theorem div_self_of_invertible {α : Type u} [GroupWithZero α] (a : α) [Invertible a] : a / a = 1

def invertibleDiv {α : Type u} [GroupWithZero α] (a : α) (b : α) [Invertible a] [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} [GroupWithZero α] (a : α) (b : α) [Invertible a] [Invertible b] [Invertible (a / b)] : ⅟(a / b) = b / a

def Invertible.map {R : Type u_1} {S : Type u_2} {F : Type u_3} [MulOneClass R] [MulOneClass S] [FunLike F R S] [MonoidHomClass F R S] (f : F) (r : R) [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} [MulOneClass R] [Monoid S] [FunLike F R S] [MonoidHomClass F R S] (f : F) (r : R) [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} [MulOneClass R] [MulOneClass S] [FunLike G S R] [MonoidHomClass G S R] (f : R → S) (g : G) (r : R) (h : Function.LeftInverse (⇑g) f) [Invertible (f r)] : ⅟r = ⅟(g (f r))

def Invertible.ofLeftInverse {R : Type u_1} {S : Type u_2} {G : Type u_3} [MulOneClass R] [MulOneClass S] [FunLike G S R] [MonoidHomClass G S R] (f : R → S) (g : G) (r : R) (h : Function.LeftInverse (⇑g) f) [Invertible (f r)] : Invertible 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} [Monoid R] [Monoid S] [FunLike F R S] [MonoidHomClass F R S] [FunLike G S R] [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} [Monoid R] [Monoid S] [FunLike F R S] [MonoidHomClass F R S] [FunLike G S R] [MonoidHomClass G S R] (f : F) (g : G) (r : R) (h : Function.LeftInverse ⇑g ⇑f) : ∀ (x : Invertible r), (invertibleEquivOfLeftInverse f g r h).symm x = Invertible.map f r

def invertibleEquivOfLeftInverse {R : Type u_1} {S : Type u_2} {F : Type u_3} {G : Type u_4} [Monoid R] [Monoid S] [FunLike F R S] [MonoidHomClass F R S] [FunLike G S R] [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.