mathlib3 documentation

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
def to_add_units {G : Type u_10} [add_group G] :

An additive group is isomorphic to its group of additive units

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) :
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ˣ) :
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]
theorem add_units.add_left_apply {M : Type u_6} [add_monoid M] (u : add_units M) :
(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
def add_units.add_left {M : Type u_6} [add_monoid M] (u : add_units M) :

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]
@[simp]
theorem units.mul_right_apply {M : Type u_6} [monoid M] (u : Mˣ) :
(u.mul_right) = λ (x : M), x * u
@[simp]
theorem add_units.add_right_apply {M : Type u_6} [add_monoid M] (u : add_units M) :
(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
def add_units.add_right {M : Type u_6} [add_monoid M] (u : add_units M) :

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)
theorem add_units.add_right_bijective {M : Type u_6} [add_monoid M] (a : add_units M) :
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]

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) :
@[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) :
(equiv.add_right a) = λ (x : G), x + a
@[simp]
theorem equiv.coe_mul_right {G : Type u_10} [group G] (a : G) :
(equiv.mul_right a) = λ (x : G), x * a
@[simp]
theorem equiv.add_right_symm {G : Type u_10} [add_group G] (a : G) :
@[simp]
@[simp, nolint]
theorem equiv.add_right_symm_apply {G : Type u_10} [add_group G] (a : G) :
(equiv.symm (equiv.add_right a)) = λ (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) :
(equiv.symm (equiv.mul_right a)) = λ (x : G), x * a⁻¹

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

theorem add_group.add_right_bijective {G : Type u_10} [add_group G] (a : G) :
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) :
@[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) :
@[simp]
theorem equiv.div_right_apply {G : Type u_10} [group G] (a b : G) :
@[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) :
@[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) :
@[simp]
theorem add_equiv.neg_apply (G : Type u_1) [subtraction_comm_monoid G] (ᾰ : G) :
(add_equiv.neg G) = -
def mul_equiv.inv (G : Type u_1) [division_comm_monoid G] :
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) [division_comm_monoid G] (ᾰ : G) :