Theorems about invertible elements

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

An Invertible element is a unit.

@[simp]

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

@[simp]

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

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

@[implicit_reducible]

instance Units.invertible {α : Type u} [Monoid α] (u : αˣ) : Invertible ↑u

Units are invertible in their associated monoid.

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

@[implicit_reducible]

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.

@[simp]

theorem nonempty_invertible_iff_isUnit {α : Type u} [Monoid α] (a : α) : Nonempty (Invertible a) ↔ IsUnit a

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

@[reducible, inline]

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

This is the Invertible version of Units.isUnit_units_mul

@[reducible, inline]

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

This is the Invertible version of Units.isUnit_mul_units

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

invertibleOfInvertibleMul and invertibleMul as an equivalence.

@[simp]

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

@[simp]

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

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

invertibleOfMulInvertible and invertibleMul as an equivalence.

@[simp]

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

@[simp]

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

@[implicit_reducible]

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

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

@[implicit_reducible]

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).

@[implicit_reducible]

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.

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.

@[implicit_reducible]

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))

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

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

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