# mathlib3documentation

algebra.hom.equiv.units.basic

# Multiplicative and additive equivalence acting on units. #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

def to_units {G : Type u_10} [group G] :
G ≃* Gˣ

A group is isomorphic to its group of units.

Equations
G ≃+

Equations
@[simp]
theorem coe_to_units {G : Type u_10} [group G] (g : G) :
@[simp]
theorem coe_to_add_units {G : Type u_10} [add_group G] (g : G) :
= g
def units.map_equiv {M : Type u_6} {N : Type u_7} [monoid M] [monoid N] (h : M ≃* N) :

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

Equations
@[simp]
theorem units.map_equiv_symm {M : Type u_6} {N : Type u_7} [monoid M] [monoid N] (h : M ≃* N) :
@[simp]
theorem units.coe_map_equiv {M : Type u_6} {N : Type u_7} [monoid M] [monoid N] (h : M ≃* N) (x : Mˣ) :
( x) = h x
def units.mul_left {M : Type u_6} [monoid M] (u : Mˣ) :

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

Equations
@[simp]
(u.add_left) = λ (x : M), u + x
@[simp]
theorem units.mul_left_apply {M : Type u_6} [monoid M] (u : Mˣ) :
(u.mul_left) = λ (x : M), u * x

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

Equations
@[simp]
theorem units.mul_left_symm {M : Type u_6} [monoid M] (u : Mˣ) :
@[simp]
theorem units.mul_left_bijective {M : Type u_6} [monoid M] (a : Mˣ) :
@[simp]
theorem units.mul_right_apply {M : Type u_6} [monoid M] (u : Mˣ) :
(u.mul_right) = λ (x : M), x * u
@[simp]
(u.add_right) = λ (x : M), x + u
def units.mul_right {M : Type u_6} [monoid M] (u : Mˣ) :

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

Equations

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

Equations
@[simp]
theorem units.mul_right_symm {M : Type u_6} [monoid M] (u : Mˣ) :
@[simp]
theorem units.mul_right_bijective {M : Type u_6} [monoid M] (a : Mˣ) :
function.bijective (λ (_x : M), _x * a)
function.bijective (λ (_x : M), _x + a)
@[protected]
def equiv.add_left {G : Type u_10} [add_group G] (a : G) :

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

Equations
@[protected]
def equiv.mul_left {G : Type u_10} [group G] (a : G) :

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

Equations
@[simp]
theorem equiv.coe_mul_left {G : Type u_10} [group G] (a : G) :
@[simp]
theorem equiv.coe_add_left {G : Type u_10} [add_group G] (a : G) :
@[simp, nolint]
theorem equiv.add_left_symm_apply {G : Type u_10} [add_group G] (a : G) :

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

@[simp, nolint]
theorem equiv.mul_left_symm_apply {G : Type u_10} [group G] (a : G) :

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

@[simp]
theorem equiv.mul_left_symm {G : Type u_10} [group G] (a : G) :
@[simp]
theorem equiv.add_left_symm {G : Type u_10} [add_group G] (a : G) :
theorem group.mul_left_bijective {G : Type u_10} [group G] (a : G) :
@[protected]
def equiv.mul_right {G : Type u_10} [group G] (a : G) :

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

Equations
@[protected]
def equiv.add_right {G : Type u_10} [add_group G] (a : G) :

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

Equations
@[simp]
theorem equiv.coe_add_right {G : Type u_10} [add_group G] (a : G) :
= λ (x : G), x + a
@[simp]
theorem equiv.coe_mul_right {G : Type u_10} [group G] (a : G) :
= λ (x : G), x * a
@[simp]
theorem equiv.add_right_symm {G : Type u_10} [add_group G] (a : G) :
@[simp]
theorem equiv.mul_right_symm {G : Type u_10} [group G] (a : G) :
@[simp, nolint]
theorem equiv.add_right_symm_apply {G : Type u_10} [add_group G] (a : G) :
= λ (x : G), x + -a

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

@[simp, nolint]
theorem equiv.mul_right_symm_apply {G : Type u_10} [group G] (a : G) :
= λ (x : G), x * a⁻¹

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

function.bijective (λ (_x : G), _x + a)
theorem group.mul_right_bijective {G : Type u_10} [group G] (a : G) :
function.bijective (λ (_x : G), _x * a)
@[protected]
def equiv.sub_left {G : Type u_10} [add_group G] (a : G) :
G G

A version of equiv.add_left a (-b) that is defeq to a - b.

Equations
@[simp]
theorem equiv.div_left_symm_apply {G : Type u_10} [group G] (a b : G) :
@[simp]
theorem equiv.div_left_apply {G : Type u_10} [group G] (a b : G) :
b = a / b
@[simp]
theorem equiv.sub_left_symm_apply {G : Type u_10} [add_group G] (a b : G) :
@[protected]
def equiv.div_left {G : Type u_10} [group G] (a : G) :
G G

A version of equiv.mul_left a b⁻¹ that is defeq to a / b.

Equations
@[simp]
theorem equiv.sub_left_apply {G : Type u_10} [add_group G] (a b : G) :
b = a - b
theorem equiv.div_left_eq_inv_trans_mul_left {G : Type u_10} [group G] (a : G) :
theorem equiv.sub_left_eq_neg_trans_add_left {G : Type u_10} [add_group G] (a : G) :
@[simp]
theorem equiv.div_right_apply {G : Type u_10} [group G] (a b : G) :
b = b / a
@[simp]
theorem equiv.sub_right_symm_apply {G : Type u_10} [add_group G] (a b : G) :
@[simp]
theorem equiv.sub_right_apply {G : Type u_10} [add_group G] (a b : G) :
b = b - a
@[protected]
def equiv.sub_right {G : Type u_10} [add_group G] (a : G) :
G G

A version of equiv.add_right (-a) b that is defeq to b - a.

Equations
@[protected]
def equiv.div_right {G : Type u_10} [group G] (a : G) :
G G

A version of equiv.mul_right a⁻¹ b that is defeq to b / a.

Equations
@[simp]
theorem equiv.div_right_symm_apply {G : Type u_10} [group G] (a b : G) :
theorem equiv.sub_right_eq_add_right_neg {G : Type u_10} [add_group G] (a : G) :
theorem equiv.div_right_eq_mul_right_inv {G : Type u_10} [group G] (a : G) :
def add_equiv.neg (G : Type u_1)  :
G ≃+ G

When the add_group is commutative, equiv.neg is an add_equiv.

Equations
@[simp]
theorem add_equiv.neg_apply (G : Type u_1) (ᾰ : G) :
= -
def mul_equiv.inv (G : Type u_1)  :
G ≃* G

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

Equations
@[simp]
theorem mul_equiv.inv_apply (G : Type u_1) (ᾰ : G) :
=⁻¹
@[simp]
theorem mul_equiv.inv_symm (G : Type u_1)  :