# Documentation

Mathlib.Algebra.Hom.Equiv.Units.Basic

# Multiplicative and additive equivalence acting on units. #

def toAddUnits.proof_1 {G : Type u_1} [inst : ] :
∀ (x : G), (fun x => x) ((fun x => { val := x, neg := -x, val_neg := (_ : x + -x = 0), neg_val := (_ : -x + x = 0) }) x) = (fun x => x) ((fun x => { val := x, neg := -x, val_neg := (_ : x + -x = 0), neg_val := (_ : -x + x = 0) }) x)
Equations
• One or more equations did not get rendered due to their size.
def toAddUnits.proof_3 {G : Type u_1} [inst : ] :
∀ (x x_1 : G), Equiv.toFun { toFun := fun x => { val := x, neg := -x, val_neg := (_ : x + -x = 0), neg_val := (_ : -x + x = 0) }, invFun := fun x => x, left_inv := (_ : ∀ (x : G), (fun x => x) ((fun x => { val := x, neg := -x, val_neg := (_ : x + -x = 0), neg_val := (_ : -x + x = 0) }) x) = (fun x => x) ((fun x => { val := x, neg := -x, val_neg := (_ : x + -x = 0), neg_val := (_ : -x + x = 0) }) x)), right_inv := (_ : ∀ (x : ), (fun x => { val := x, neg := -x, val_neg := (_ : x + -x = 0), neg_val := (_ : -x + x = 0) }) ((fun x => x) x) = x) } (x + x_1) = Equiv.toFun { toFun := fun x => { val := x, neg := -x, val_neg := (_ : x + -x = 0), neg_val := (_ : -x + x = 0) }, invFun := fun x => x, left_inv := (_ : ∀ (x : G), (fun x => x) ((fun x => { val := x, neg := -x, val_neg := (_ : x + -x = 0), neg_val := (_ : -x + x = 0) }) x) = (fun x => x) ((fun x => { val := x, neg := -x, val_neg := (_ : x + -x = 0), neg_val := (_ : -x + x = 0) }) x)), right_inv := (_ : ∀ (x : ), (fun x => { val := x, neg := -x, val_neg := (_ : x + -x = 0), neg_val := (_ : -x + x = 0) }) ((fun x => x) x) = x) } x + Equiv.toFun { toFun := fun x => { val := x, neg := -x, val_neg := (_ : x + -x = 0), neg_val := (_ : -x + x = 0) }, invFun := fun x => x, left_inv := (_ : ∀ (x : G), (fun x => x) ((fun x => { val := x, neg := -x, val_neg := (_ : x + -x = 0), neg_val := (_ : -x + x = 0) }) x) = (fun x => x) ((fun x => { val := x, neg := -x, val_neg := (_ : x + -x = 0), neg_val := (_ : -x + x = 0) }) x)), right_inv := (_ : ∀ (x : ), (fun x => { val := x, neg := -x, val_neg := (_ : x + -x = 0), neg_val := (_ : -x + x = 0) }) ((fun x => x) x) = x) } x_1
Equations
• One or more equations did not get rendered due to their size.
def toAddUnits.proof_2 {G : Type u_1} [inst : ] :
∀ (x : ), (fun x => { val := x, neg := -x, val_neg := (_ : x + -x = 0), neg_val := (_ : -x + x = 0) }) ((fun x => x) x) = x
Equations
• One or more equations did not get rendered due to their size.
def toAddUnits {G : Type u_1} [inst : ] :
G ≃+

Equations
• One or more equations did not get rendered due to their size.
def toUnits {G : Type u_1} [inst : ] :
G ≃* Gˣ

A group is isomorphic to its group of units.

Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem coe_toAddUnits {G : Type u_1} [inst : ] (g : G) :
@[simp]
theorem coe_toUnits {G : Type u_1} [inst : ] (g : G) :
↑(toUnits g) = g
def Units.mapEquiv {M : Type u_1} {N : Type u_2} [inst : ] [inst : ] (h : M ≃* N) :

A multiplicative equivalence of monoids defines a multiplicative equivalence of their groups of units.

Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem Units.mapEquiv_symm {M : Type u_1} {N : Type u_2} [inst : ] [inst : ] (h : M ≃* N) :
@[simp]
theorem Units.coe_mapEquiv {M : Type u_1} {N : Type u_2} [inst : ] [inst : ] (h : M ≃* N) (x : Mˣ) :
↑(↑() x) = h x
def AddUnits.addLeft {M : Type u_1} [inst : ] (u : ) :

Left addition of an additive unit is a permutation of the underlying type.

Equations
• = { toFun := fun x => u + x, invFun := fun x => ↑(-u) + x, left_inv := (_ : ∀ (b : M), ↑(-u) + (u + b) = b), right_inv := (_ : ∀ (b : M), u + (↑(-u) + b) = b) }
@[simp]
theorem AddUnits.addLeft_apply {M : Type u_1} [inst : ] (u : ) :
↑() = fun x => u + x
@[simp]
theorem Units.mulLeft_apply {M : Type u_1} [inst : ] (u : Mˣ) :
↑() = fun x => u * x
def Units.mulLeft {M : Type u_1} [inst : ] (u : Mˣ) :

Left multiplication by a unit of a monoid is a permutation of the underlying type.

Equations
• = { toFun := fun x => u * x, invFun := fun x => u⁻¹ * x, left_inv := (_ : ∀ (b : M), u⁻¹ * (u * b) = b), right_inv := (_ : ∀ (b : M), u * (u⁻¹ * b) = b) }
@[simp]
theorem AddUnits.addLeft_symm {M : Type u_1} [inst : ] (u : ) :
@[simp]
theorem Units.mulLeft_symm {M : Type u_1} [inst : ] (u : Mˣ) :
theorem AddUnits.addLeft_bijective {M : Type u_1} [inst : ] (a : ) :
Function.Bijective fun x => a + x
theorem Units.mulLeft_bijective {M : Type u_1} [inst : ] (a : Mˣ) :
Function.Bijective fun x => a * x
def AddUnits.addRight.proof_2 {M : Type u_1} [inst : ] (u : ) (x : M) :
x + ↑(-u) + u = x
Equations
• (_ : x + ↑(-u) + u = x) = (_ : x + ↑(-u) + u = x)
def AddUnits.addRight {M : Type u_1} [inst : ] (u : ) :

Right addition of an additive unit is a permutation of the underlying type.

Equations
• = { toFun := fun x => x + u, invFun := fun x => x + ↑(-u), left_inv := (_ : ∀ (x : M), x + u + ↑(-u) = x), right_inv := (_ : ∀ (x : M), x + ↑(-u) + u = x) }
def AddUnits.addRight.proof_1 {M : Type u_1} [inst : ] (u : ) (x : M) :
x + u + ↑(-u) = x
Equations
• (_ : x + u + ↑(-u) = x) = (_ : x + u + ↑(-u) = x)
@[simp]
theorem AddUnits.addRight_apply {M : Type u_1} [inst : ] (u : ) :
↑() = fun x => x + u
@[simp]
theorem Units.mulRight_apply {M : Type u_1} [inst : ] (u : Mˣ) :
↑() = fun x => x * u
def Units.mulRight {M : Type u_1} [inst : ] (u : Mˣ) :

Right multiplication by a unit of a monoid is a permutation of the underlying type.

Equations
• = { toFun := fun x => x * u, invFun := fun x => x * u⁻¹, left_inv := (_ : ∀ (x : M), x * u * u⁻¹ = x), right_inv := (_ : ∀ (x : M), x * u⁻¹ * u = x) }
@[simp]
theorem AddUnits.addRight_symm {M : Type u_1} [inst : ] (u : ) :
@[simp]
theorem Units.mulRight_symm {M : Type u_1} [inst : ] (u : Mˣ) :
theorem AddUnits.addRight_bijective {M : Type u_1} [inst : ] (a : ) :
Function.Bijective fun x => x + a
theorem Units.mulRight_bijective {M : Type u_1} [inst : ] (a : Mˣ) :
Function.Bijective fun x => x * a
def Equiv.addLeft {G : Type u_1} [inst : ] (a : G) :

Left addition in an AddGroup is a permutation of the underlying type.

Equations
def Equiv.mulLeft {G : Type u_1} [inst : ] (a : G) :

Left multiplication in a Group is a permutation of the underlying type.

Equations
@[simp]
theorem Equiv.coe_addLeft {G : Type u_1} [inst : ] (a : G) :
↑() = (fun x x_1 => x + x_1) a
@[simp]
theorem Equiv.coe_mulLeft {G : Type u_1} [inst : ] (a : G) :
↑() = (fun x x_1 => x * x_1) a
theorem Equiv.addLeft_symm_apply {G : Type u_1} [inst : ] (a : G) :
↑() = fun x => -a + x

Extra simp lemma that dsimp can use. simp will never use this.

@[simp]
theorem Equiv.mulLeft_symm_apply {G : Type u_1} [inst : ] (a : G) :
↑() = fun x => a⁻¹ * x

Extra simp lemma that dsimp can use. simp will never use this.

@[simp]
theorem Equiv.addLeft_symm {G : Type u_1} [inst : ] (a : G) :
@[simp]
theorem Equiv.mulLeft_symm {G : Type u_1} [inst : ] (a : G) :
theorem AddGroup.addLeft_bijective {G : Type u_1} [inst : ] (a : G) :
Function.Bijective fun x => a + x
theorem Group.mulLeft_bijective {G : Type u_1} [inst : ] (a : G) :
Function.Bijective fun x => a * x
def Equiv.addRight {G : Type u_1} [inst : ] (a : G) :

Right addition in an AddGroup is a permutation of the underlying type.

Equations
def Equiv.mulRight {G : Type u_1} [inst : ] (a : G) :

Right multiplication in a Group is a permutation of the underlying type.

Equations
@[simp]
theorem Equiv.coe_addRight {G : Type u_1} [inst : ] (a : G) :
↑() = fun x => x + a
@[simp]
theorem Equiv.coe_mulRight {G : Type u_1} [inst : ] (a : G) :
↑() = fun x => x * a
@[simp]
theorem Equiv.addRight_symm {G : Type u_1} [inst : ] (a : G) :
@[simp]
theorem Equiv.mulRight_symm {G : Type u_1} [inst : ] (a : G) :
theorem Equiv.addRight_symm_apply {G : Type u_1} [inst : ] (a : G) :
↑() = fun x => x + -a

Extra simp lemma that dsimp can use. simp will never use this.

@[simp]
theorem Equiv.mulRight_symm_apply {G : Type u_1} [inst : ] (a : G) :
↑() = fun x => x * a⁻¹

Extra simp lemma that dsimp can use. simp will never use this.

theorem AddGroup.addRight_bijective {G : Type u_1} [inst : ] (a : G) :
Function.Bijective fun x => x + a
theorem Group.mulRight_bijective {G : Type u_1} [inst : ] (a : G) :
Function.Bijective fun x => x * a
def Equiv.subLeft.proof_2 {G : Type u_1} [inst : ] (a : G) (b : G) :
a - (-b + a) = b
Equations
• (_ : a - (-b + a) = b) = (_ : a - (-b + a) = b)
def Equiv.subLeft.proof_1 {G : Type u_1} [inst : ] (a : G) (b : G) :
-(a - b) + a = b
Equations
• (_ : -(a - b) + a = b) = (_ : -(a - b) + a = b)
def Equiv.subLeft {G : Type u_1} [inst : ] (a : G) :
G G

A version of Equiv.addLeft a (-b) that is defeq to a - b.

Equations
• = { toFun := fun b => a - b, invFun := fun b => -b + a, left_inv := (_ : ∀ (b : G), -(a - b) + a = b), right_inv := (_ : ∀ (b : G), a - (-b + a) = b) }
@[simp]
theorem Equiv.divLeft_symm_apply {G : Type u_1} [inst : ] (a : G) (b : G) :
↑() b = b⁻¹ * a
@[simp]
theorem Equiv.divLeft_apply {G : Type u_1} [inst : ] (a : G) (b : G) :
↑() b = a / b
@[simp]
theorem Equiv.subLeft_symm_apply {G : Type u_1} [inst : ] (a : G) (b : G) :
↑() b = -b + a
@[simp]
theorem Equiv.subLeft_apply {G : Type u_1} [inst : ] (a : G) (b : G) :
↑() b = a - b
def Equiv.divLeft {G : Type u_1} [inst : ] (a : G) :
G G

A version of Equiv.mulLeft a b⁻¹⁻¹ that is defeq to a / b.

Equations
• = { toFun := fun b => a / b, invFun := fun b => b⁻¹ * a, left_inv := (_ : ∀ (b : G), (a / b)⁻¹ * a = b), right_inv := (_ : ∀ (b : G), a / (b⁻¹ * a) = b) }
theorem Equiv.subLeft_eq_neg_trans_addLeft {G : Type u_1} [inst : ] (a : G) :
= Equiv.trans () ()
theorem Equiv.divLeft_eq_inv_trans_mulLeft {G : Type u_1} [inst : ] (a : G) :
= Equiv.trans () ()
def Equiv.subRight {G : Type u_1} [inst : ] (a : G) :
G G

A version of Equiv.addRight (-a) b that is defeq to b - a.

Equations
• = { toFun := fun b => b - a, invFun := fun b => b + a, left_inv := (_ : ∀ (b : G), b - a + a = b), right_inv := (_ : ∀ (b : G), b + a - a = b) }
def Equiv.subRight.proof_2 {G : Type u_1} [inst : ] (a : G) (b : G) :
b + a - a = b
Equations
• (_ : b + a - a = b) = (_ : b + a - a = b)
def Equiv.subRight.proof_1 {G : Type u_1} [inst : ] (a : G) (b : G) :
b - a + a = b
Equations
• (_ : b - a + a = b) = (_ : b - a + a = b)
@[simp]
theorem Equiv.subRight_symm_apply {G : Type u_1} [inst : ] (a : G) (b : G) :
↑() b = b + a
@[simp]
theorem Equiv.divRight_apply {G : Type u_1} [inst : ] (a : G) (b : G) :
↑() b = b / a
@[simp]
theorem Equiv.divRight_symm_apply {G : Type u_1} [inst : ] (a : G) (b : G) :
↑() b = b * a
@[simp]
theorem Equiv.subRight_apply {G : Type u_1} [inst : ] (a : G) (b : G) :
↑() b = b - a
def Equiv.divRight {G : Type u_1} [inst : ] (a : G) :
G G

A version of Equiv.mulRight a⁻¹ b⁻¹ b that is defeq to b / a.

Equations
• = { toFun := fun b => b / a, invFun := fun b => b * a, left_inv := (_ : ∀ (b : G), b / a * a = b), right_inv := (_ : ∀ (b : G), b * a / a = b) }
theorem Equiv.subRight_eq_addRight_neg {G : Type u_1} [inst : ] (a : G) :
theorem Equiv.divRight_eq_mulRight_inv {G : Type u_1} [inst : ] (a : G) :
def AddEquiv.neg (G : Type u_1) [inst : ] :
G ≃+ G

When the AddGroup is commutative, Equiv.neg is an AddEquiv.

Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem AddEquiv.neg_apply (G : Type u_1) [inst : ] :
∀ (a : G), ↑() a = -a
@[simp]
theorem MulEquiv.inv_apply (G : Type u_1) [inst : ] :
∀ (a : G), ↑() a = a⁻¹
def MulEquiv.inv (G : Type u_1) [inst : ] :
G ≃* G

In a DivisionCommMonoid, Equiv.inv is a MulEquiv. There is a variant of this MulEquiv.inv' G : G ≃* Gᵐᵒᵖ≃* Gᵐᵒᵖ for the non-commutative case.

Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem AddEquiv.neg_symm (G : Type u_1) [inst : ] :
@[simp]
theorem MulEquiv.inv_symm (G : Type u_1) [inst : ] :