# Documentation

Mathlib.Algebra.Invertible.Basic

# Theorems about invertible elements #

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

An Invertible element is a unit.

Instances For
theorem isUnit_of_invertible {α : Type u} [] (a : α) [] :
def Units.invertible {α : Type u} [] (u : αˣ) :

Units are invertible in their associated monoid.

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.

Instances For
@[simp]
theorem nonempty_invertible_iff_isUnit {α : Type u} [] (a : α) :
def invertibleNeg {α : Type u} [Mul α] [One α] [] (a : α) [] :

-⅟a is the inverse of -a

Instances For
@[simp]
theorem invOf_neg {α : Type u} [] [] (a : α) [] [Invertible (-a)] :
(-a) = -a
@[simp]
theorem one_sub_invOf_two {α : Type u} [Ring α] [] :
1 - 2 = 2
@[simp]
theorem invOf_two_add_invOf_two {α : Type u} [] [] :
2 + 2 = 1
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) [] :
theorem pos_of_invertible_cast {α : Type u} [] [] (n : ) [] :
0 < n
@[reducible]
def invertibleOfInvertibleMul {α : Type u} [] (a : α) (b : α) [] [Invertible (a * b)] :

This is the Invertible version of Units.isUnit_units_mul

Instances For
@[reducible]
def invertibleOfMulInvertible {α : Type u} [] (a : α) (b : α) [Invertible (a * b)] [] :

This is the Invertible version of Units.isUnit_mul_units

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

invertibleOfInvertibleMul and invertibleMul as an equivalence.

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.

Instances For
@[simp]
theorem Ring.inverse_invertible {α : Type u} [] (x : α) [] :

A variant of Ring.inverse_unit.

@[simp]
theorem div_mul_cancel_of_invertible {α : Type u} [] (a : α) (b : α) [] :
a / b * b = a
@[simp]
theorem mul_div_cancel_of_invertible {α : Type u} [] (a : α) (b : α) [] :
a * b / b = a
@[simp]
theorem div_self_of_invertible {α : Type u} [] (a : α) [] :
a / a = 1
def invertibleDiv {α : Type u} [] (a : α) (b : α) [] [] :

b / a is the inverse of a / b

Instances For
theorem invOf_div {α : Type u} [] (a : α) (b : α) [] [] [Invertible (a / b)] :
(a / b) = b / a
def Invertible.map {R : Type u_1} {S : Type u_2} {F : Type u_3} [] [] [] (f : F) (r : R) [] :
Invertible (f r)

Monoid homs preserve invertibility.

Instances For
theorem map_invOf {R : Type u_1} {S : Type u_2} {F : Type u_3} [] [] [] (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} [] [] [] (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} [] [] [] (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))

Instances For
@[simp]
theorem invertibleEquivOfLeftInverse_symm_apply {R : Type u_1} {S : Type u_2} {F : Type u_3} {G : Type u_4} [] [] [] [] (f : F) (g : G) (r : R) (h : ) :
∀ (x : ), ().symm x =
@[simp]
theorem invertibleEquivOfLeftInverse_apply {R : Type u_1} {S : Type u_2} {F : Type u_3} {G : Type u_4} [] [] [] [] (f : F) (g : G) (r : R) (h : ) :
∀ (x : Invertible (f r)), ↑() x = Invertible.ofLeftInverse (f) g r h
def invertibleEquivOfLeftInverse {R : Type u_1} {S : Type u_2} {F : Type u_3} {G : Type u_4} [] [] [] [] (f : F) (g : G) (r : R) (h : ) :
Invertible (f r)

Invertibility on either side of a monoid hom with a left-inverse is equivalent.

Instances For