# Multiplicative and additive equivalence acting on units. #

theorem toAddUnits.proof_1 {G : Type u_1} [] :
∀ (x : G), (fun (x : ) => x) ((fun (x : G) => { val := x, neg := -x, val_neg := , neg_val := }) x) = (fun (x : ) => x) ((fun (x : G) => { val := x, neg := -x, val_neg := , neg_val := }) x)
def toAddUnits {G : Type u_10} [] :
G ≃+

Equations
• toAddUnits = { toFun := fun (x : G) => { val := x, neg := -x, val_neg := , neg_val := }, invFun := fun (x : ) => x, left_inv := , right_inv := , map_add' := }
Instances For
theorem toAddUnits.proof_3 {G : Type u_1} [] :
∀ (x x_1 : G), { toFun := fun (x : G) => { val := x, neg := -x, val_neg := , neg_val := }, invFun := fun (x : ) => x, left_inv := , right_inv := }.toFun (x + x_1) = { toFun := fun (x : G) => { val := x, neg := -x, val_neg := , neg_val := }, invFun := fun (x : ) => x, left_inv := , right_inv := }.toFun x + { toFun := fun (x : G) => { val := x, neg := -x, val_neg := , neg_val := }, invFun := fun (x : ) => x, left_inv := , right_inv := }.toFun x_1
theorem toAddUnits.proof_2 {G : Type u_1} [] :
∀ (x : ), (fun (x : G) => { val := x, neg := -x, val_neg := , neg_val := }) ((fun (x : ) => x) x) = x
@[simp]
theorem val_toAddUnits_apply {G : Type u_10} [] (x : G) :
@[simp]
theorem toAddUnits_symm_apply {G : Type u_10} [] (x : ) :
@[simp]
theorem val_toUnits_apply {G : Type u_10} [] (x : G) :
(toUnits x) = x
@[simp]
theorem toUnits_symm_apply {G : Type u_10} [] (x : Gˣ) :
toUnits.symm x = x
def toUnits {G : Type u_10} [] :
G ≃* Gˣ

A group is isomorphic to its group of units.

Equations
• toUnits = { toFun := fun (x : G) => { val := x, inv := x⁻¹, val_inv := , inv_val := }, invFun := fun (x : Gˣ) => x, left_inv := , right_inv := , map_mul' := }
Instances For
@[simp]
theorem toAddUnits_val_apply {G : Type u_12} [] (x : ) :
@[simp]
theorem toUnits_val_apply {G : Type u_12} [] (x : Gˣ) :
toUnits x = x
def Units.mapEquiv {M : Type u_6} {N : Type u_7} [] [] (h : M ≃* N) :

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

Equations
• = { toFun := (↑(Units.map h.toMonoidHom)).toFun, invFun := (Units.map h.symm.toMonoidHom), left_inv := , right_inv := , map_mul' := }
Instances For
@[simp]
theorem Units.mapEquiv_symm {M : Type u_6} {N : Type u_7} [] [] (h : M ≃* N) :
.symm = Units.mapEquiv h.symm
@[simp]
theorem Units.coe_mapEquiv {M : Type u_6} {N : Type u_7} [] [] (h : M ≃* N) (x : Mˣ) :
( x) = h x

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

Equations
• u.addLeft = { toFun := fun (x : M) => u + x, invFun := fun (x : M) => (-u) + x, left_inv := , right_inv := }
Instances For
@[simp]
theorem Units.mulLeft_apply {M : Type u_6} [] (u : Mˣ) :
u.mulLeft = fun (x : M) => u * x
@[simp]
u.addLeft = fun (x : M) => u + x
def Units.mulLeft {M : Type u_6} [] (u : Mˣ) :

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

Equations
• u.mulLeft = { toFun := fun (x : M) => u * x, invFun := fun (x : M) => u⁻¹ * x, left_inv := , right_inv := }
Instances For
@[simp]
@[simp]
theorem Units.mulLeft_symm {M : Type u_6} [] (u : Mˣ) :
Equiv.symm u.mulLeft = u⁻¹.mulLeft
Function.Bijective fun (x : M) => a + x
theorem Units.mulLeft_bijective {M : Type u_6} [] (a : Mˣ) :
Function.Bijective fun (x : M) => a * x

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

Equations
• u.addRight = { toFun := fun (x : M) => x + u, invFun := fun (x : M) => x + (-u), left_inv := , right_inv := }
Instances For
@[simp]
theorem Units.mulRight_apply {M : Type u_6} [] (u : Mˣ) :
u.mulRight = fun (x : M) => x * u
@[simp]
u.addRight = fun (x : M) => x + u
def Units.mulRight {M : Type u_6} [] (u : Mˣ) :

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

Equations
• u.mulRight = { toFun := fun (x : M) => x * u, invFun := fun (x : M) => x * u⁻¹, left_inv := , right_inv := }
Instances For
@[simp]
@[simp]
theorem Units.mulRight_symm {M : Type u_6} [] (u : Mˣ) :
Equiv.symm u.mulRight = u⁻¹.mulRight
Function.Bijective fun (x : M) => x + a
theorem Units.mulRight_bijective {M : Type u_6} [] (a : Mˣ) :
Function.Bijective fun (x : M) => x * a
def Equiv.addLeft {G : Type u_10} [] (a : G) :

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

Equations
Instances For
def Equiv.mulLeft {G : Type u_10} [] (a : G) :

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

Equations
• = (toUnits a).mulLeft
Instances For
@[simp]
theorem Equiv.coe_addLeft {G : Type u_10} [] (a : G) :
= fun (x : G) => a + x
@[simp]
theorem Equiv.coe_mulLeft {G : Type u_10} [] (a : G) :
= fun (x : G) => a * x
theorem Equiv.addLeft_symm_apply {G : Type u_10} [] (a : G) :
(Equiv.symm ) = fun (x : G) => -a + x

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

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

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

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

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

Equations
Instances For
def Equiv.mulRight {G : Type u_10} [] (a : G) :

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

Equations
• = (toUnits a).mulRight
Instances For
@[simp]
theorem Equiv.coe_addRight {G : Type u_10} [] (a : G) :
= fun (x : G) => x + a
@[simp]
theorem Equiv.coe_mulRight {G : Type u_10} [] (a : G) :
= fun (x : G) => x * a
@[simp]
theorem Equiv.addRight_symm {G : Type u_10} [] (a : G) :
@[simp]
theorem Equiv.mulRight_symm {G : Type u_10} [] (a : G) :
theorem Equiv.addRight_symm_apply {G : Type u_10} [] (a : G) :
(Equiv.symm ) = fun (x : G) => x + -a

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

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

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

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

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

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

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

Equations
• = { toFun := fun (b : G) => a / b, invFun := fun (b : G) => b⁻¹ * a, left_inv := , right_inv := }
Instances For
theorem Equiv.subLeft_eq_neg_trans_addLeft {G : Type u_10} [] (a : G) :
=
theorem Equiv.divLeft_eq_inv_trans_mulLeft {G : Type u_10} [] (a : G) :
=
theorem Equiv.subRight.proof_1 {G : Type u_1} [] (a : G) (b : G) :
b - a + a = b
def Equiv.subRight {G : Type u_10} [] (a : G) :
G G

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

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

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

Equations
• = { toFun := fun (b : G) => b / a, invFun := fun (b : G) => b * a, left_inv := , right_inv := }
Instances For
theorem Equiv.subRight_eq_addRight_neg {G : Type u_10} [] (a : G) :
theorem Equiv.divRight_eq_mulRight_inv {G : Type u_10} [] (a : G) :
@[simp]
theorem unitsEquivProdSubtype_apply_coe (α : Type u_2) [] (u : αˣ) :
( u) = (u, u⁻¹)
@[simp]
theorem val_unitsEquivProdSubtype_symm_apply (α : Type u_2) [] (p : { p : α × α // p.1 * p.2 = 1 p.2 * p.1 = 1 }) :
(.symm p) = (↑p).1
@[simp]
theorem val_inv_unitsEquivProdSubtype_symm_apply (α : Type u_2) [] (p : { p : α × α // p.1 * p.2 = 1 p.2 * p.1 = 1 }) :
(.symm p)⁻¹ = (↑p).2
def unitsEquivProdSubtype (α : Type u_2) [] :
αˣ { p : α × α // p.1 * p.2 = 1 p.2 * p.1 = 1 }

The αˣ type is equivalent to a subtype of α × α.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def AddEquiv.neg (G : Type u_12) :
G ≃+ G

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

Equations
• = { toFun := Neg.neg, invFun := Neg.neg, left_inv := , right_inv := , map_add' := }
Instances For
@[simp]
theorem AddEquiv.neg_apply (G : Type u_12) :
∀ (a : G), (AddEquiv.neg G) a = -a
@[simp]
theorem MulEquiv.inv_apply (G : Type u_12) :
∀ (a : G), (MulEquiv.inv G) a = a⁻¹
def MulEquiv.inv (G : Type u_12) :
G ≃* G

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

Equations
• = { toFun := Inv.inv, invFun := Inv.inv, left_inv := , right_inv := , map_mul' := }
Instances For
@[simp]
theorem AddEquiv.neg_symm (G : Type u_12) :