mathlib documentation

data.equiv.mul_add

Multiplicative and additive equivs

In this file we define two extensions of equiv called add_equiv and mul_equiv, which are datatypes representing isomorphisms of add_monoids/add_groups and monoids/groups. We also introduce the corresponding groups of automorphisms add_aut and mul_aut.

Notations

The extended equivs all have coercions to functions, and the coercions are the canonical notation when treating the isomorphisms as maps.

Implementation notes

The fields for mul_equiv, add_equiv now avoid the unbundled is_mul_hom and is_add_hom, as these are deprecated.

Definition of multiplication in the groups of automorphisms agrees with function composition, multiplication in equiv.perm, and multiplication in category_theory.End, not with category_theory.comp.

Tags

equiv, mul_equiv, add_equiv, mul_aut, add_aut

def add_equiv.to_equiv {A : Type u_8} {B : Type u_9} [has_add A] [has_add B] :
A ≃+ BA B

The equiv underlying an add_equiv.

structure add_equiv (A : Type u_8) (B : Type u_9) [has_add A] [has_add B] :
Type (max u_8 u_9)

add_equiv α β is the type of an equiv α ≃ β which preserves addition.

def add_equiv.to_add_hom {A : Type u_8} {B : Type u_9} [has_add A] [has_add B] :
A ≃+ Badd_hom A B

The add_hom underlying a add_equiv.

def mul_equiv.to_mul_hom {M : Type u_8} {N : Type u_9} [has_mul M] [has_mul N] :
M ≃* Nmul_hom M N

The mul_hom underlying a mul_equiv.

def mul_equiv.to_equiv {M : Type u_8} {N : Type u_9} [has_mul M] [has_mul N] :
M ≃* NM N

The equiv underlying a mul_equiv.

structure mul_equiv (M : Type u_8) (N : Type u_9) [has_mul M] [has_mul N] :
Type (max u_8 u_9)

mul_equiv α β is the type of an equiv α ≃ β which preserves multiplication.

@[instance]
def add_equiv.has_coe_to_fun {M : Type u_3} {N : Type u_4} [has_add M] [has_add N] :

@[instance]
def mul_equiv.has_coe_to_fun {M : Type u_3} {N : Type u_4} [has_mul M] [has_mul N] :

Equations
@[simp]
theorem mul_equiv.to_fun_apply {M : Type u_3} {N : Type u_4} [has_mul M] [has_mul N] {f : M ≃* N} {m : M} :
f.to_fun m = f m

@[simp]
theorem add_equiv.to_fun_apply {M : Type u_3} {N : Type u_4} [has_add M] [has_add N] {f : M ≃+ N} {m : M} :
f.to_fun m = f m

@[simp]
theorem add_equiv.to_equiv_apply {M : Type u_3} {N : Type u_4} [has_add M] [has_add N] {f : M ≃+ N} {m : M} :
(f.to_equiv) m = f m

@[simp]
theorem mul_equiv.to_equiv_apply {M : Type u_3} {N : Type u_4} [has_mul M] [has_mul N] {f : M ≃* N} {m : M} :
(f.to_equiv) m = f m

@[simp]
theorem add_equiv.map_add {M : Type u_3} {N : Type u_4} [has_add M] [has_add N] (f : M ≃+ N) (x y : M) :
f (x + y) = f x + f y

@[simp]
theorem mul_equiv.map_mul {M : Type u_3} {N : Type u_4} [has_mul M] [has_mul N] (f : M ≃* N) (x y : M) :
f (x * y) = (f x) * f y

A multiplicative isomorphism preserves multiplication (canonical form).

@[instance]
def mul_equiv.is_mul_hom {M : Type u_3} {N : Type u_4} [has_mul M] [has_mul N] (h : M ≃* N) :

A multiplicative isomorphism preserves multiplication (deprecated).

@[instance]
def add_equiv.is_add_hom {M : Type u_3} {N : Type u_4} [has_add M] [has_add N] (h : M ≃+ N) :

def add_equiv.mk' {M : Type u_3} {N : Type u_4} [has_add M] [has_add N] (f : M N) :
(∀ (x y : M), f (x + y) = f x + f y)M ≃+ N

Makes an additive isomorphism from a bijection which preserves addition.

def mul_equiv.mk' {M : Type u_3} {N : Type u_4} [has_mul M] [has_mul N] (f : M N) :
(∀ (x y : M), f (x * y) = (f x) * f y)M ≃* N

Makes a multiplicative isomorphism from a bijection which preserves multiplication.

Equations
theorem add_equiv.bijective {M : Type u_3} {N : Type u_4} [has_add M] [has_add N] (e : M ≃+ N) :

theorem mul_equiv.bijective {M : Type u_3} {N : Type u_4} [has_mul M] [has_mul N] (e : M ≃* N) :

theorem mul_equiv.injective {M : Type u_3} {N : Type u_4} [has_mul M] [has_mul N] (e : M ≃* N) :

theorem add_equiv.injective {M : Type u_3} {N : Type u_4} [has_add M] [has_add N] (e : M ≃+ N) :

theorem mul_equiv.surjective {M : Type u_3} {N : Type u_4} [has_mul M] [has_mul N] (e : M ≃* N) :

theorem add_equiv.surjective {M : Type u_3} {N : Type u_4} [has_add M] [has_add N] (e : M ≃+ N) :

def add_equiv.refl (M : Type u_1) [has_add M] :
M ≃+ M

The identity map is an additive isomorphism.

def mul_equiv.refl (M : Type u_1) [has_mul M] :
M ≃* M

The identity map is a multiplicative isomorphism.

Equations
@[instance]
def mul_equiv.inhabited {M : Type u_3} [has_mul M] :

Equations
def add_equiv.symm {M : Type u_3} {N : Type u_4} [has_add M] [has_add N] :
M ≃+ NN ≃+ M

The inverse of an isomorphism is an isomorphism.

def mul_equiv.symm {M : Type u_3} {N : Type u_4} [has_mul M] [has_mul N] :
M ≃* NN ≃* M

The inverse of an isomorphism is an isomorphism.

Equations
@[simp]
theorem mul_equiv.to_equiv_symm {M : Type u_3} {N : Type u_4} [has_mul M] [has_mul N] (f : M ≃* N) :

@[simp]
theorem add_equiv.to_equiv_symm {M : Type u_3} {N : Type u_4} [has_add M] [has_add N] (f : M ≃+ N) :

@[simp]
theorem mul_equiv.coe_mk {M : Type u_3} {N : Type u_4} [has_mul M] [has_mul N] (f : M → N) (g : N → M) (h₁ : function.left_inverse g f) (h₂ : function.right_inverse g f) (h₃ : ∀ (x y : M), f (x * y) = (f x) * f y) :
{to_fun := f, inv_fun := g, left_inv := h₁, right_inv := h₂, map_mul' := h₃} = f

@[simp]
theorem add_equiv.coe_mk {M : Type u_3} {N : Type u_4} [has_add M] [has_add N] (f : M → N) (g : N → M) (h₁ : function.left_inverse g f) (h₂ : function.right_inverse g f) (h₃ : ∀ (x y : M), f (x + y) = f x + f y) :
{to_fun := f, inv_fun := g, left_inv := h₁, right_inv := h₂, map_add' := h₃} = f

@[simp]
theorem add_equiv.coe_symm_mk {M : Type u_3} {N : Type u_4} [has_add M] [has_add N] (f : M → N) (g : N → M) (h₁ : function.left_inverse g f) (h₂ : function.right_inverse g f) (h₃ : ∀ (x y : M), f (x + y) = f x + f y) :
({to_fun := f, inv_fun := g, left_inv := h₁, right_inv := h₂, map_add' := h₃}.symm) = g

@[simp]
theorem mul_equiv.coe_symm_mk {M : Type u_3} {N : Type u_4} [has_mul M] [has_mul N] (f : M → N) (g : N → M) (h₁ : function.left_inverse g f) (h₂ : function.right_inverse g f) (h₃ : ∀ (x y : M), f (x * y) = (f x) * f y) :
({to_fun := f, inv_fun := g, left_inv := h₁, right_inv := h₂, map_mul' := h₃}.symm) = g

def mul_equiv.trans {M : Type u_3} {N : Type u_4} {P : Type u_5} [has_mul M] [has_mul N] [has_mul P] :
M ≃* NN ≃* PM ≃* P

Transitivity of multiplication-preserving isomorphisms

Equations
def add_equiv.trans {M : Type u_3} {N : Type u_4} {P : Type u_5} [has_add M] [has_add N] [has_add P] :
M ≃+ NN ≃+ PM ≃+ P

Transitivity of addition-preserving isomorphisms

@[simp]
theorem mul_equiv.apply_symm_apply {M : Type u_3} {N : Type u_4} [has_mul M] [has_mul N] (e : M ≃* N) (y : N) :
e ((e.symm) y) = y

e.right_inv in canonical form

@[simp]
theorem add_equiv.apply_symm_apply {M : Type u_3} {N : Type u_4} [has_add M] [has_add N] (e : M ≃+ N) (y : N) :
e ((e.symm) y) = y

@[simp]
theorem mul_equiv.symm_apply_apply {M : Type u_3} {N : Type u_4} [has_mul M] [has_mul N] (e : M ≃* N) (x : M) :
(e.symm) (e x) = x

e.left_inv in canonical form

@[simp]
theorem add_equiv.symm_apply_apply {M : Type u_3} {N : Type u_4} [has_add M] [has_add N] (e : M ≃+ N) (x : M) :
(e.symm) (e x) = x

@[simp]
theorem add_equiv.refl_apply {M : Type u_3} [has_add M] (m : M) :

@[simp]
theorem mul_equiv.refl_apply {M : Type u_3} [has_mul M] (m : M) :

@[simp]
theorem mul_equiv.trans_apply {M : Type u_3} {N : Type u_4} {P : Type u_5} [has_mul M] [has_mul N] [has_mul P] (e₁ : M ≃* N) (e₂ : N ≃* P) (m : M) :
(e₁.trans e₂) m = e₂ (e₁ m)

@[simp]
theorem add_equiv.trans_apply {M : Type u_3} {N : Type u_4} {P : Type u_5} [has_add M] [has_add N] [has_add P] (e₁ : M ≃+ N) (e₂ : N ≃+ P) (m : M) :
(e₁.trans e₂) m = e₂ (e₁ m)

@[simp]
theorem add_equiv.apply_eq_iff_eq {M : Type u_3} {N : Type u_4} [has_add M] [has_add N] (e : M ≃+ N) {x y : M} :
e x = e y x = y

@[simp]
theorem mul_equiv.apply_eq_iff_eq {M : Type u_3} {N : Type u_4} [has_mul M] [has_mul N] (e : M ≃* N) {x y : M} :
e x = e y x = y

theorem add_equiv.apply_eq_iff_symm_apply {M : Type u_3} {N : Type u_4} [has_add M] [has_add N] (e : M ≃+ N) {x : M} {y : N} :
e x = y x = (e.symm) y

theorem mul_equiv.apply_eq_iff_symm_apply {M : Type u_3} {N : Type u_4} [has_mul M] [has_mul N] (e : M ≃* N) {x : M} {y : N} :
e x = y x = (e.symm) y

theorem add_equiv.symm_apply_eq {M : Type u_3} {N : Type u_4} [has_add M] [has_add N] (e : M ≃+ N) {x : N} {y : M} :
(e.symm) x = y x = e y

theorem mul_equiv.symm_apply_eq {M : Type u_3} {N : Type u_4} [has_mul M] [has_mul N] (e : M ≃* N) {x : N} {y : M} :
(e.symm) x = y x = e y

theorem mul_equiv.eq_symm_apply {M : Type u_3} {N : Type u_4} [has_mul M] [has_mul N] (e : M ≃* N) {x : N} {y : M} :
y = (e.symm) x e y = x

theorem add_equiv.eq_symm_apply {M : Type u_3} {N : Type u_4} [has_add M] [has_add N] (e : M ≃+ N) {x : N} {y : M} :
y = (e.symm) x e y = x

@[simp]
theorem add_equiv.map_zero {M : Type u_1} {N : Type u_2} [add_monoid M] [add_monoid N] (h : M ≃+ N) :
h 0 = 0

@[simp]
theorem mul_equiv.map_one {M : Type u_1} {N : Type u_2} [monoid M] [monoid N] (h : M ≃* N) :
h 1 = 1

a multiplicative equiv of monoids sends 1 to 1 (and is hence a monoid isomorphism)

@[simp]
theorem add_equiv.map_eq_zero_iff {M : Type u_1} {N : Type u_2} [add_monoid M] [add_monoid N] (h : M ≃+ N) {x : M} :
h x = 0 x = 0

@[simp]
theorem mul_equiv.map_eq_one_iff {M : Type u_1} {N : Type u_2} [monoid M] [monoid N] (h : M ≃* N) {x : M} :
h x = 1 x = 1

theorem add_equiv.map_ne_zero_iff {M : Type u_1} {N : Type u_2} [add_monoid M] [add_monoid N] (h : M ≃+ N) {x : M} :
h x 0 x 0

theorem mul_equiv.map_ne_one_iff {M : Type u_1} {N : Type u_2} [monoid M] [monoid N] (h : M ≃* N) {x : M} :
h x 1 x 1

def add_equiv.of_bijective {M : Type u_1} {N : Type u_2} [add_monoid M] [add_monoid N] (f : M →+ N) :

A bijective add_monoid homomorphism is an isomorphism

def mul_equiv.of_bijective {M : Type u_1} {N : Type u_2} [monoid M] [monoid N] (f : M →* N) :

A bijective monoid homomorphism is an isomorphism

Equations
def add_equiv.to_add_monoid_hom {M : Type u_1} {N : Type u_2} [add_monoid M] [add_monoid N] :
M ≃+ NM →+ N

Extract the forward direction of an additive equivalence as an addition-preserving function.

def mul_equiv.to_monoid_hom {M : Type u_1} {N : Type u_2} [monoid M] [monoid N] :
M ≃* NM →* N

Extract the forward direction of a multiplicative equivalence as a multiplication-preserving function.

Equations
@[simp]
theorem mul_equiv.coe_to_monoid_hom {M : Type u_1} {N : Type u_2} [monoid M] [monoid N] (e : M ≃* N) :

@[simp]
theorem add_equiv.coe_to_add_monoid_hom {M : Type u_1} {N : Type u_2} [add_monoid M] [add_monoid N] (e : M ≃+ N) :

theorem add_equiv.to_add_monoid_hom_apply {M : Type u_1} {N : Type u_2} [add_monoid M] [add_monoid N] (e : M ≃+ N) (x : M) :

theorem mul_equiv.to_monoid_hom_apply {M : Type u_1} {N : Type u_2} [monoid M] [monoid N] (e : M ≃* N) (x : M) :

@[simp]
theorem add_equiv.map_neg {G : Type u_6} {H : Type u_7} [add_group G] [add_group H] (h : G ≃+ H) (x : G) :
h (-x) = -h x

@[simp]
theorem mul_equiv.map_inv {G : Type u_6} {H : Type u_7} [group G] [group H] (h : G ≃* H) (x : G) :

A multiplicative equivalence of groups preserves inversion.

@[instance]
def add_equiv.is_add_monoid_hom {M : Type u_1} {N : Type u_2} [add_monoid M] [add_monoid N] (h : M ≃+ N) :

@[instance]
def mul_equiv.is_monoid_hom {M : Type u_1} {N : Type u_2} [monoid M] [monoid N] (h : M ≃* N) :

A multiplicative bijection between two monoids is a monoid hom (deprecated -- use to_monoid_hom).

@[instance]
def add_equiv.is_add_group_hom {G : Type u_1} {H : Type u_2} [add_group G] [add_group H] (h : G ≃+ H) :

@[instance]
def mul_equiv.is_group_hom {G : Type u_1} {H : Type u_2} [group G] [group H] (h : G ≃* H) :

A multiplicative bijection between two groups is a group hom (deprecated -- use to_monoid_hom).

@[ext]
theorem add_equiv.ext {M : Type u_3} {N : Type u_4} [has_add M] [has_add N] {f g : M ≃+ N} :
(∀ (x : M), f x = g x)f = g

Two additive isomorphisms agree if they are defined by the same underlying function.

@[ext]
theorem mul_equiv.ext {M : Type u_3} {N : Type u_4} [has_mul M] [has_mul N] {f g : M ≃* N} :
(∀ (x : M), f x = g x)f = g

Two multiplicative isomorphisms agree if they are defined by the same underlying function.

def add_monoid_hom.to_add_equiv {M : Type u_3} {N : Type u_4} [add_monoid M] [add_monoid N] (f : M →+ N) (g : N →+ M) :

Given a pair of additive monoid homomorphisms f, g such that g.comp f = id and f.comp g = id, returns an additive equivalence with to_fun = f and inv_fun = g. This constructor is useful if the underlying type(s) have specialized ext lemmas for additive monoid homomorphisms.

Equations
def monoid_hom.to_mul_equiv {M : Type u_3} {N : Type u_4} [monoid M] [monoid N] (f : M →* N) (g : N →* M) :
g.comp f = monoid_hom.id Mf.comp g = monoid_hom.id NM ≃* N

Given a pair of monoid homomorphisms f, g such that g.comp f = id and f.comp g = id, returns an multiplicative equivalence with to_fun = f and inv_fun = g. This constructor is useful if the underlying type(s) have specialized ext lemmas for monoid homomorphisms.

Equations
@[simp]
theorem add_monoid_hom.coe_to_add_equiv {M : Type u_3} {N : Type u_4} [add_monoid M] [add_monoid N] (f : M →+ N) (g : N →+ M) (h₁ : g.comp f = add_monoid_hom.id M) (h₂ : f.comp g = add_monoid_hom.id N) :
(f.to_add_equiv g h₁ h₂) = f

@[simp]
theorem monoid_hom.coe_to_mul_equiv {M : Type u_3} {N : Type u_4} [monoid M] [monoid N] (f : M →* N) (g : N →* M) (h₁ : g.comp f = monoid_hom.id M) (h₂ : f.comp g = monoid_hom.id N) :
(f.to_mul_equiv g h₁ h₂) = f

theorem add_equiv.map_sub {A : Type u_1} {B : Type u_2} [add_group A] [add_group B] (h : A ≃+ B) (x y : A) :
h (x - y) = h x - h y

An additive equivalence of additive groups preserves subtraction.

@[instance]
def add_equiv.inhabited {M : Type u_1} [has_add M] :

Equations
def mul_aut (M : Type u_1) [has_mul M] :
Type u_1

The group of multiplicative automorphisms.

Equations
def add_aut (M : Type u_1) [has_add M] :
Type u_1

The group of additive automorphisms.

@[instance]
def mul_aut.group (M : Type u_3) [has_mul M] :

The group operation on multiplicative automorphisms is defined by λ g h, mul_equiv.trans h g. This means that multiplication agrees with composition, (g*h)(x) = g (h x).

Equations
@[instance]
def mul_aut.inhabited (M : Type u_3) [has_mul M] :

Equations
@[simp]
theorem mul_aut.coe_mul (M : Type u_3) [has_mul M] (e₁ e₂ : mul_aut M) :
e₁ * e₂ = e₁ e₂

@[simp]
theorem mul_aut.coe_one (M : Type u_3) [has_mul M] :

theorem mul_aut.mul_def (M : Type u_3) [has_mul M] (e₁ e₂ : mul_aut M) :
e₁ * e₂ = mul_equiv.trans e₂ e₁

theorem mul_aut.one_def (M : Type u_3) [has_mul M] :

theorem mul_aut.inv_def (M : Type u_3) [has_mul M] (e₁ : mul_aut M) :

@[simp]
theorem mul_aut.mul_apply (M : Type u_3) [has_mul M] (e₁ e₂ : mul_aut M) (m : M) :
(e₁ * e₂) m = e₁ (e₂ m)

@[simp]
theorem mul_aut.one_apply (M : Type u_3) [has_mul M] (m : M) :
1 m = m

@[simp]
theorem mul_aut.apply_inv_self (M : Type u_3) [has_mul M] (e : mul_aut M) (m : M) :
e (e⁻¹ m) = m

@[simp]
theorem mul_aut.inv_apply_self (M : Type u_3) [has_mul M] (e : mul_aut M) (m : M) :
e⁻¹ (e m) = m

def mul_aut.to_perm (M : Type u_3) [has_mul M] :

Monoid hom from the group of multiplicative automorphisms to the group of permutations.

Equations
def mul_aut.conj {G : Type u_6} [group G] :

group conjugation as a group homomorphism into the automorphism group. conj g h = g * h * g⁻¹

Equations
@[simp]
theorem mul_aut.conj_apply {G : Type u_6} [group G] (g h : G) :

@[simp]
theorem mul_aut.conj_symm_apply {G : Type u_6} [group G] (g h : G) :

@[simp]
theorem mul_aut.conj_inv_apply {G : Type u_1} [group G] (g h : G) :

@[instance]
def add_aut.group (A : Type u_1) [has_add A] :

The group operation on additive automorphisms is defined by λ g h, mul_equiv.trans h g. This means that multiplication agrees with composition, (g*h)(x) = g (h x).

Equations
@[instance]
def add_aut.inhabited (A : Type u_1) [has_add A] :

Equations
@[simp]
theorem add_aut.coe_mul (A : Type u_1) [has_add A] (e₁ e₂ : add_aut A) :
e₁ * e₂ = e₁ e₂

@[simp]
theorem add_aut.coe_one (A : Type u_1) [has_add A] :

theorem add_aut.mul_def (A : Type u_1) [has_add A] (e₁ e₂ : add_aut A) :
e₁ * e₂ = add_equiv.trans e₂ e₁

theorem add_aut.one_def (A : Type u_1) [has_add A] :

theorem add_aut.inv_def (A : Type u_1) [has_add A] (e₁ : add_aut A) :

@[simp]
theorem add_aut.mul_apply (A : Type u_1) [has_add A] (e₁ e₂ : add_aut A) (a : A) :
(e₁ * e₂) a = e₁ (e₂ a)

@[simp]
theorem add_aut.one_apply (A : Type u_1) [has_add A] (a : A) :
1 a = a

@[simp]
theorem add_aut.apply_inv_self (A : Type u_1) [has_add A] (e : add_aut A) (a : A) :
e⁻¹ (e a) = a

@[simp]
theorem add_aut.inv_apply_self (A : Type u_1) [has_add A] (e : add_aut A) (a : A) :
e (e⁻¹ a) = a

def add_aut.to_perm (A : Type u_1) [has_add A] :

Monoid hom from the group of multiplicative automorphisms to the group of permutations.

Equations
def to_units {G : Type u_1} [group G] :

A group is isomorphic to its group of units.

Equations
def to_add_units {G : Type u_1} [add_group G] :

An additive group is isomorphic to its group of additive units

def units.map_equiv {M : Type u_3} {N : Type u_4} [monoid M] [monoid N] :
M ≃* Nunits M ≃* units N

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

Equations
def units.mul_left {M : Type u_3} [monoid M] :

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

Equations
def add_units.add_left {M : Type u_3} [add_monoid M] :

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

@[simp]
theorem units.coe_mul_left {M : Type u_3} [monoid M] (u : units M) :

@[simp]
theorem add_units.coe_add_left {M : Type u_3} [add_monoid M] (u : add_units M) :

@[simp]
theorem units.mul_left_symm {M : Type u_3} [monoid M] (u : units M) :

@[simp]
theorem add_units.add_left_symm {M : Type u_3} [add_monoid M] (u : add_units M) :

def units.mul_right {M : Type u_3} [monoid 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_3} [add_monoid M] :

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

@[simp]
theorem add_units.coe_add_right {M : Type u_3} [add_monoid M] (u : add_units M) :
(u.add_right) = λ (x : M), x + u

@[simp]
theorem units.coe_mul_right {M : Type u_3} [monoid M] (u : units M) :
(u.mul_right) = λ (x : M), x * u

@[simp]
theorem units.mul_right_symm {M : Type u_3} [monoid M] (u : units M) :

@[simp]
theorem add_units.add_right_symm {M : Type u_3} [add_monoid M] (u : add_units M) :

def equiv.add_left {G : Type u_6} [add_group G] :
G → equiv.perm G

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

def equiv.mul_left {G : Type u_6} [group G] :
G → equiv.perm G

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

Equations
@[simp]
theorem equiv.coe_mul_left {G : Type u_6} [group G] (a : G) :

@[simp]
theorem equiv.coe_add_left {G : Type u_6} [add_group G] (a : G) :

@[simp]
theorem equiv.mul_left_symm {G : Type u_6} [group G] (a : G) :

@[simp]
theorem equiv.add_left_symm {G : Type u_6} [add_group G] (a : G) :

def equiv.mul_right {G : Type u_6} [group G] :
G → equiv.perm G

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

Equations
def equiv.add_right {G : Type u_6} [add_group G] :
G → equiv.perm G

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

@[simp]
theorem equiv.coe_add_right {G : Type u_6} [add_group G] (a : G) :
(equiv.add_right a) = λ (x : G), x + a

@[simp]
theorem equiv.coe_mul_right {G : Type u_6} [group G] (a : G) :
(equiv.mul_right a) = λ (x : G), x * a

@[simp]
theorem equiv.add_right_symm {G : Type u_6} [add_group G] (a : G) :

@[simp]
theorem equiv.mul_right_symm {G : Type u_6} [group G] (a : G) :

def equiv.neg (G : Type u_6) [add_group G] :

Negation on an add_group is a permutation of the underlying type.

def equiv.inv (G : Type u_6) [group G] :

Inversion on a group is a permutation of the underlying type.

Equations
@[simp]
theorem equiv.coe_inv {G : Type u_6} [group G] :

@[simp]
theorem equiv.coe_neg {G : Type u_6} [add_group G] :

@[simp]
theorem equiv.neg_symm {G : Type u_6} [add_group G] :

@[simp]
theorem equiv.inv_symm {G : Type u_6} [group G] :

def equiv.point_reflection {A : Type u_1} [add_comm_group A] :
A → equiv.perm A

Point reflection in x as a permutation.

Equations
theorem equiv.point_reflection_apply {A : Type u_1} [add_comm_group A] (x y : A) :

@[simp]
theorem equiv.point_reflection_self {A : Type u_1} [add_comm_group A] (x : A) :

x is the only fixed point of point_reflection x. This lemma requires x + x = y + y ↔ x = y. There is no typeclass to use here, so we add it as an explicit argument.

def mul_equiv.to_additive {G : Type u_6} {H : Type u_7} [monoid G] [monoid H] :

Reinterpret G ≃* H as additive G ≃+ additive H.

Equations
def mul_equiv.to_additive' {G : Type u_6} {H : Type u_7} [monoid G] [add_monoid H] :

Reinterpret G ≃* multiplicative H as additive G ≃+ H as.

Equations
def mul_equiv.to_additive'' {G : Type u_6} {H : Type u_7} [add_monoid G] [monoid H] :

Reinterpret multiplicative G ≃* H as G ≃+ additive H as.

Equations