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

source
def add_equiv.to_equiv {A : Type u_8} {B : Type u_9} [has_add A] [has_add B] (s : A ≃+ B) :
A ≃ B

The equiv underlying an add_equiv.

source
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.

source
def mul_equiv.to_equiv {M : Type u_8} {N : Type u_9} [has_mul M] [has_mul N] (s : M ≃* N) :
M ≃ N

The equiv underlying a mul_equiv.

source
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.

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

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

Equations
source
@[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

source
@[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

source
@[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

source
@[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

source
@[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

source
@[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).

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

A multiplicative isomorphism preserves multiplication (deprecated).

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

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

Makes an additive isomorphism from a bijection which preserves addition.

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

Makes a multiplicative isomorphism from a bijection which preserves multiplication.

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

The identity map is an additive isomorphism.

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

The identity map is a multiplicative isomorphism.

Equations
source
@[instance]
def mul_equiv.inhabited {M : Type u_3} [has_mul M] :
inhabited (M ≃* M)

Equations
source
def add_equiv.symm {M : Type u_3} {N : Type u_4} [has_add M] [has_add N] (h : M ≃+ N) :
N ≃+ M

The inverse of an isomorphism is an isomorphism.

source
def mul_equiv.symm {M : Type u_3} {N : Type u_4} [has_mul M] [has_mul N] (h : M ≃* N) :
N ≃* M

The inverse of an isomorphism is an isomorphism.

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

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

source
@[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

source
@[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

source
@[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

source
@[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

source
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] (h1 : M ≃* N) (h2 : N ≃* P) :
M ≃* P

Transitivity of multiplication-preserving isomorphisms

Equations
source
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] (h1 : M ≃+ N) (h2 : N ≃+ P) :
M ≃+ P

Transitivity of addition-preserving isomorphisms

source
@[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

source
@[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

source
@[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

source
@[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

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

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

source
@[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)

source
@[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)

source
@[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

source
@[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)

source
@[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

source
@[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

source
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

source
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

source
def add_equiv.of_bijective {M : Type u_1} {N : Type u_2} [add_monoid M] [add_monoid N] (f : M →+ N) (hf : function.bijective ⇑f) :
M ≃+ N

A bijective add_monoid homomorphism is an isomorphism

source
def mul_equiv.of_bijective {M : Type u_1} {N : Type u_2} [monoid M] [monoid N] (f : M →* N) (hf : function.bijective ⇑f) :
M ≃* N

A bijective monoid homomorphism is an isomorphism

Equations
source
def add_equiv.to_add_monoid_hom {M : Type u_1} {N : Type u_2} [add_monoid M] [add_monoid N] (h : M ≃+ N) :
M →+ N

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

source
def mul_equiv.to_monoid_hom {M : Type u_1} {N : Type u_2} [monoid M] [monoid N] (h : M ≃* N) :
M →* N

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

Equations
source
@[simp]
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) :
⇑(e.to_add_monoid_hom) x = ⇑e x

source
@[simp]
theorem mul_equiv.to_monoid_hom_apply {M : Type u_1} {N : Type u_2} [monoid M] [monoid N] (e : M ≃* N) (x : M) :
⇑(e.to_monoid_hom) x = ⇑e x

source
@[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

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

A multiplicative equivalence of groups preserves inversion.

source
@[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) :
is_add_monoid_hom ⇑h

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

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

source
@[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) :
is_add_group_hom ⇑h

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

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

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

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

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

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

source
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.

source
@[instance]
def add_equiv.inhabited {M : Type u_1} [has_add M] :
inhabited (M ≃+ M)

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

The group of multiplicative automorphisms.

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

The group of additive automorphisms.

source
@[instance]
def mul_aut.group (M : Type u_3) [has_mul M] :
group (mul_aut 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
source
@[instance]
def mul_aut.inhabited (M : Type u_3) [has_mul M] :
inhabited (mul_aut M)

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

source
@[simp]
theorem mul_aut.coe_one (M : Type u_3) [has_mul M] :
⇑1 = id

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

source
theorem mul_aut.one_def (M : Type u_3) [has_mul M] :
1 = mul_equiv.refl M

source
theorem mul_aut.inv_def (M : Type u_3) [has_mul M] (e₁ : mul_aut M) :
e₁⁻¹ = mul_equiv.symm e₁

source
@[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)

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

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

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

source
def mul_aut.to_perm (M : Type u_3) [has_mul M] :
mul_aut M →* equiv.perm M

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

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

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

Equations
source
@[simp]
theorem mul_aut.conj_apply {G : Type u_6} [group G] (g h : G) :
⇑(⇑mul_aut.conj g) h = (g * h) * g⁻¹

source
@[simp]
theorem mul_aut.conj_symm_apply {G : Type u_6} [group G] (g h : G) :
⇑(mul_equiv.symm (⇑mul_aut.conj g)) h = (g⁻¹ * h) * g

source
@[simp]
theorem mul_aut.conj_inv_apply {G : Type u_1} [group G] (g h : G) :
⇑(⇑mul_aut.conj g)⁻¹ h = (g⁻¹ * h) * g

source
@[instance]
def add_aut.group (A : Type u_1) [has_add A] :
group (add_aut 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
source
@[instance]
def add_aut.inhabited (A : Type u_1) [has_add A] :
inhabited (add_aut A)

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

source
@[simp]
theorem add_aut.coe_one (A : Type u_1) [has_add A] :
⇑1 = id

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

source
theorem add_aut.one_def (A : Type u_1) [has_add A] :
1 = add_equiv.refl A

source
theorem add_aut.inv_def (A : Type u_1) [has_add A] (e₁ : add_aut A) :
e₁⁻¹ = add_equiv.symm e₁

source
@[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)

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

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

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

source
def add_aut.to_perm (A : Type u_1) [has_add A] :
add_aut A →* equiv.perm A

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

Equations
source
def to_units {G : Type u_1} [group G] :
G ≃* units G

A group is isomorphic to its group of units.

Equations
source
def to_add_units {G : Type u_1} [add_group G] :
G ≃+ add_units G

An additive group is isomorphic to its group of additive units

source
def units.map_equiv {M : Type u_3} {N : Type u_4} [monoid M] [monoid N] (h : M ≃* N) :
units M ≃* units N

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

Equations
source
def units.mul_left {M : Type u_3} [monoid M] (u : units M) :
equiv.perm M

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

Equations
source
def add_units.add_left {M : Type u_3} [add_monoid M] (u : add_units M) :
equiv.perm M

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

source
@[simp]
theorem units.coe_mul_left {M : Type u_3} [monoid M] (u : units M) :
⇑(u.mul_left) = has_mul.mul ↑u

source
@[simp]
theorem add_units.coe_add_left {M : Type u_3} [add_monoid M] (u : add_units M) :
⇑(u.add_left) = has_add.add ↑u

source
@[simp]
theorem units.mul_left_symm {M : Type u_3} [monoid M] (u : units M) :
equiv.symm u.mul_left = u⁻¹.mul_left

source
@[simp]
theorem add_units.add_left_symm {M : Type u_3} [add_monoid M] (u : add_units M) :
equiv.symm u.add_left = (-u).add_left

source
def units.mul_right {M : Type u_3} [monoid M] (u : units M) :
equiv.perm M

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

Equations
source
def add_units.add_right {M : Type u_3} [add_monoid M] (u : add_units M) :
equiv.perm M

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

source
@[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

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

source
@[simp]
theorem units.mul_right_symm {M : Type u_3} [monoid M] (u : units M) :
equiv.symm u.mul_right = u⁻¹.mul_right

source
@[simp]
theorem add_units.add_right_symm {M : Type u_3} [add_monoid M] (u : add_units M) :
equiv.symm u.add_right = (-u).add_right

source
def equiv.add_left {G : Type u_6} [add_group G] (a : G) :
equiv.perm G

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

source
def equiv.mul_left {G : Type u_6} [group G] (a : G) :
equiv.perm G

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

Equations
source
@[simp]
theorem equiv.coe_mul_left {G : Type u_6} [group G] (a : G) :
⇑(equiv.mul_left a) = has_mul.mul a

source
@[simp]
theorem equiv.coe_add_left {G : Type u_6} [add_group G] (a : G) :
⇑(equiv.add_left a) = has_add.add a

source
@[simp]
theorem equiv.mul_left_symm {G : Type u_6} [group G] (a : G) :
equiv.symm (equiv.mul_left a) = equiv.mul_left a⁻¹

source
@[simp]
theorem equiv.add_left_symm {G : Type u_6} [add_group G] (a : G) :
equiv.symm (equiv.add_left a) = equiv.add_left (-a)

source
def equiv.mul_right {G : Type u_6} [group G] (a : G) :
equiv.perm G

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

Equations
source
def equiv.add_right {G : Type u_6} [add_group G] (a : G) :
equiv.perm G

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

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

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

source
@[simp]
theorem equiv.add_right_symm {G : Type u_6} [add_group G] (a : G) :
equiv.symm (equiv.add_right a) = equiv.add_right (-a)

source
@[simp]
theorem equiv.mul_right_symm {G : Type u_6} [group G] (a : G) :
equiv.symm (equiv.mul_right a) = equiv.mul_right a⁻¹

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

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

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

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

Equations
source
@[simp]
theorem equiv.coe_inv {G : Type u_6} [group G] :
⇑(equiv.inv G) = has_inv.inv

source
@[simp]
theorem equiv.coe_neg {G : Type u_6} [add_group G] :
⇑(equiv.neg G) = has_neg.neg

source
@[simp]
theorem equiv.neg_symm {G : Type u_6} [add_group G] :
equiv.symm (equiv.neg G) = equiv.neg G

source
@[simp]
theorem equiv.inv_symm {G : Type u_6} [group G] :
equiv.symm (equiv.inv G) = equiv.inv G

source
def equiv.point_reflection {A : Type u_1} [add_comm_group A] (x : A) :
equiv.perm A

Point reflection in x as a permutation.

Equations
source
theorem equiv.point_reflection_apply {A : Type u_1} [add_comm_group A] (x y : A) :
⇑(equiv.point_reflection x) y = x + x - y

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

source
theorem equiv.point_reflection_involutive {A : Type u_1} [add_comm_group A] (x : A) :
function.involutive ⇑(equiv.point_reflection x)

source
@[simp]
theorem equiv.point_reflection_symm {A : Type u_1} [add_comm_group A] (x : A) :
equiv.symm (equiv.point_reflection x) = equiv.point_reflection x

source
theorem equiv.point_reflection_fixed_iff_of_bit0_injective {A : Type u_1} [add_comm_group A] {x y : A} (h : function.injective bit0) :
⇑(equiv.point_reflection x) y = y ↔ y = x

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.

source
def add_equiv.to_multiplicative {G : Type u_6} {H : Type u_7} [add_monoid G] [add_monoid H] (f : G ≃+ H) :
multiplicative G ≃* multiplicative H

Reinterpret f : G ≃+ H as multiplicative G ≃* multiplicative H.

Equations
source
def mul_equiv.to_additive {G : Type u_6} {H : Type u_7} [monoid G] [monoid H] (f : G ≃* H) :
additive G ≃+ additive H

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

Equations