# Theorems about invertible elements #

@[simp]
theorem val_unitOfInvertible {α : Type u} [] (a : α) [] :
() = a
@[simp]
theorem val_inv_unitOfInvertible {α : Type u} [] (a : α) [] :
= a
def unitOfInvertible {α : Type u} [] (a : α) [] :
αˣ

An Invertible element is a unit.

Equations
• = { val := a, inv := a, val_inv := , inv_val := }
Instances For
theorem isUnit_of_invertible {α : Type u} [] (a : α) [] :
def Units.invertible {α : Type u} [] (u : αˣ) :

Units are invertible in their associated monoid.

Equations
• u.invertible = { invOf := u⁻¹, invOf_mul_self := , mul_invOf_self := }
Instances For
@[simp]
theorem invOf_units {α : Type u} [] (u : αˣ) [] :
u = u⁻¹
theorem IsUnit.nonempty_invertible {α : Type u} [] {a : α} (h : ) :
noncomputable def IsUnit.invertible {α : Type u} [] {a : α} (h : ) :

Convert IsUnit to Invertible using Classical.choice.

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

Equations
• h.invertible =
Instances For
@[simp]
theorem nonempty_invertible_iff_isUnit {α : Type u} [] (a : α) :
theorem Commute.invOf_right {α : Type u} [] {a : α} {b : α} [] (h : Commute a b) :
theorem Commute.invOf_left {α : Type u} [] {a : α} {b : α} [] (h : Commute b a) :
theorem commute_invOf {M : Type u_1} [One M] [Mul M] (m : M) [] :
@[reducible, inline]
abbrev invertibleOfInvertibleMul {α : Type u} [] (a : α) (b : α) [] [Invertible (a * b)] :

This is the Invertible version of Units.isUnit_units_mul

Equations
• = { invOf := (a * b) * a, invOf_mul_self := , mul_invOf_self := }
Instances For
@[reducible, inline]
abbrev invertibleOfMulInvertible {α : Type u} [] (a : α) (b : α) [Invertible (a * b)] [] :

This is the Invertible version of Units.isUnit_mul_units

Equations
• = { invOf := b * (a * b), invOf_mul_self := , mul_invOf_self := }
Instances For
@[simp]
theorem Invertible.mulLeft_symm_apply {α : Type u} [] {a : α} :
∀ (x : ) (b : α) (x_1 : Invertible (a * b)), (x.mulLeft b).symm x_1 =
@[simp]
theorem Invertible.mulLeft_apply {α : Type u} [] {a : α} :
∀ (x : ) (b : α) (x_1 : ), (x.mulLeft b) x_1 =
def Invertible.mulLeft {α : Type u} [] {a : α} :
(b : α) → Invertible (a * b)

invertibleOfInvertibleMul and invertibleMul as an equivalence.

Equations
• x.mulLeft b = { toFun := fun (x_1 : ) => , invFun := fun (x_1 : Invertible (a * b)) => , left_inv := , right_inv := }
Instances For
@[simp]
theorem Invertible.mulRight_symm_apply {α : Type u} [] (a : α) {b : α} :
∀ (x : ) (x_1 : Invertible (a * b)), ().symm x_1 =
@[simp]
theorem Invertible.mulRight_apply {α : Type u} [] (a : α) {b : α} :
∀ (x : ) (x_1 : ), () x_1 =
def Invertible.mulRight {α : Type u} [] (a : α) {b : α} :
Invertible (a * b)

invertibleOfMulInvertible and invertibleMul as an equivalence.

Equations
• = { toFun := fun (x_1 : ) => , invFun := fun (x_1 : Invertible (a * b)) => , left_inv := , right_inv := }
Instances For
instance invertiblePow {α : Type u} [] (m : α) [] (n : ) :
Equations
• = { invOf := m ^ n, invOf_mul_self := , mul_invOf_self := }
theorem invOf_pow {α : Type u} [] (m : α) [] (n : ) [Invertible (m ^ n)] :
(m ^ n) = m ^ n
def invertibleOfPowEqOne {α : Type u} [] (x : α) (n : ) (hx : x ^ n = 1) (hn : n 0) :

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

Equations
Instances For
def Invertible.map {R : Type u_1} {S : Type u_2} {F : Type u_3} [] [] [FunLike F R S] [] (f : F) (r : R) [] :

Monoid homs preserve invertibility.

Equations
• = { invOf := f r, invOf_mul_self := , mul_invOf_self := }
Instances For
theorem map_invOf {R : Type u_1} {S : Type u_2} {F : Type u_3} [] [] [FunLike F R S] [] (f : F) (r : 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} [] [] [FunLike G S R] [] (f : RS) (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} [] [] [FunLike G S R] [] (f : RS) (g : G) (r : R) (h : Function.LeftInverse (g) f) [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
Instances For
@[simp]
theorem invertibleEquivOfLeftInverse_apply {R : Type u_1} {S : Type u_2} {F : Type u_3} {G : Type u_4} [] [] [FunLike F R S] [] [FunLike G S R] [] (f : F) (g : G) (r : R) (h : ) :
∀ (x : Invertible (f r)), () 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} [] [] [FunLike F R S] [] [FunLike G S R] [] (f : F) (g : G) (r : R) (h : ) :
∀ (x : ), ().symm x =
def invertibleEquivOfLeftInverse {R : Type u_1} {S : Type u_2} {F : Type u_3} {G : Type u_4} [] [] [FunLike F R S] [] [FunLike G S R] [] (f : F) (g : G) (r : R) (h : ) :

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.
Instances For