# mathlib3documentation

algebra.hom.equiv.basic

# Multiplicative and additive equivs #

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

In this file we define two extensions of `equiv` called `add_equiv` and `mul_equiv`, which are datatypes representing isomorphisms of `add_monoid`s/`add_group`s and `monoid`s/`group`s.

## Notations #

• `infix ` ≃* `:25 := mul_equiv`
• `infix ` ≃+ `:25 := add_equiv`

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.

## Tags #

def add_hom.inverse {M : Type u_6} {N : Type u_7} [has_add M] [has_add N] (f : N) (g : N M) (h₁ : f) (h₂ : f) :
M

Makes an additive inverse from a bijection which preserves addition.

Equations
def mul_hom.inverse {M : Type u_6} {N : Type u_7} [has_mul M] [has_mul N] (f : M →ₙ* N) (g : N M) (h₁ : f) (h₂ : f) :

Makes a multiplicative inverse from a bijection which preserves multiplication.

Equations
def add_monoid_hom.inverse {A : Type u_1} {B : Type u_2} [add_monoid A] [add_monoid B] (f : A →+ B) (g : B A) (h₁ : f) (h₂ : f) :
B →+ A

The inverse of a bijective `add_monoid_hom` is an `add_monoid_hom`.

Equations
def monoid_hom.inverse {A : Type u_1} {B : Type u_2} [monoid A] [monoid B] (f : A →* B) (g : B A) (h₁ : f) (h₂ : f) :
B →* A

The inverse of a bijective `monoid_hom` is a `monoid_hom`.

Equations
@[simp]
theorem add_monoid_hom.inverse_apply {A : Type u_1} {B : Type u_2} [add_monoid A] [add_monoid B] (f : A →+ B) (g : B A) (h₁ : f) (h₂ : f) (ᾰ : B) :
(f.inverse g h₁ h₂) = g ᾰ
@[simp]
theorem monoid_hom.inverse_apply {A : Type u_1} {B : Type u_2} [monoid A] [monoid B] (f : A →* B) (g : B A) (h₁ : f) (h₂ : f) (ᾰ : B) :
(f.inverse g h₁ h₂) = g ᾰ
def add_equiv.to_equiv {A : Type u_12} {B : Type u_13} [has_add A] [has_add B] (self : A ≃+ B) :
A B

The `equiv` underlying an `add_equiv`.

structure add_equiv (A : Type u_12) (B : Type u_13) [has_add A] [has_add B] :
Type (max u_12 u_13)

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

Instances for `add_equiv`
def add_equiv.to_add_hom {A : Type u_12} {B : Type u_13} [has_add A] [has_add B] (self : A ≃+ B) :
B

The `add_hom` underlying a `add_equiv`.

@[instance]
def add_equiv_class.to_equiv_like (F : Type u_12) (A : Type u_13) (B : Type u_14) [has_add A] [has_add B] [self : B] :
A B
@[class]
structure add_equiv_class (F : Type u_12) (A : Type u_13) (B : Type u_14) [has_add A] [has_add B] :
Type (max u_12 u_13 u_14)
• coe : F A B
• inv : F B A
• left_inv : (e : F),
• right_inv : (e : F),
• coe_injective' : (e g : F),
• map_add : (f : F) (a b : A), f (a + b) = f a + f b

`add_equiv_class F A B` states that `F` is a type of addition-preserving morphisms. You should extend this class when you extend `add_equiv`.

Instances of this typeclass
Instances of other typeclasses for `add_equiv_class`
def mul_equiv.to_mul_hom {M : Type u_12} {N : Type u_13} [has_mul M] [has_mul N] (self : M ≃* N) :

The `mul_hom` underlying a `mul_equiv`.

def mul_equiv.to_equiv {M : Type u_12} {N : Type u_13} [has_mul M] [has_mul N] (self : M ≃* N) :
M N

The `equiv` underlying a `mul_equiv`.

structure mul_equiv (M : Type u_12) (N : Type u_13) [has_mul M] [has_mul N] :
Type (max u_12 u_13)

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

Instances for `mul_equiv`
@[class]
structure mul_equiv_class (F : Type u_12) (A : Type u_13) (B : Type u_14) [has_mul A] [has_mul B] :
Type (max u_12 u_13 u_14)
• coe : F A B
• inv : F B A
• left_inv : (e : F),
• right_inv : (e : F),
• coe_injective' : (e g : F),
• map_mul : (f : F) (a b : A), f (a * b) = f a * f b

`mul_equiv_class F A B` states that `F` is a type of multiplication-preserving morphisms. You should extend this class when you extend `mul_equiv`.

Instances of this typeclass
Instances of other typeclasses for `mul_equiv_class`
• mul_equiv_class.has_sizeof_inst
@[instance]
def mul_equiv_class.to_equiv_like (F : Type u_12) (A : Type u_13) (B : Type u_14) [has_mul A] [has_mul B] [self : B] :
A B
@[protected, instance]
def mul_equiv_class.mul_hom_class (F : Type u_1) {M : Type u_6} {N : Type u_7} [has_mul M] [has_mul N] [h : N] :
N
Equations
@[protected, instance]
def add_equiv_class.add_hom_class (F : Type u_1) {M : Type u_6} {N : Type u_7} [has_add M] [has_add N] [h : N] :
N
Equations
@[protected, instance]
def mul_equiv_class.monoid_hom_class (F : Type u_1) {M : Type u_6} {N : Type u_7} [ N] :
N
Equations
@[protected, instance]
def add_equiv_class.add_monoid_hom_class (F : Type u_1) {M : Type u_6} {N : Type u_7} [ N] :
N
Equations
@[protected, instance]
def mul_equiv_class.to_monoid_with_zero_hom_class (F : Type u_1) {α : Type u_2} {β : Type u_3} [ β] :
Equations
@[simp]
theorem add_equiv_class.map_eq_zero_iff {F : Type u_1} {M : Type u_2} {N : Type u_3} [ N] (h : F) {x : M} :
h x = 0 x = 0
@[simp]
theorem mul_equiv_class.map_eq_one_iff {F : Type u_1} {M : Type u_2} {N : Type u_3} [ N] (h : F) {x : M} :
h x = 1 x = 1
theorem mul_equiv_class.map_ne_one_iff {F : Type u_1} {M : Type u_2} {N : Type u_3} [ N] (h : F) {x : M} :
h x 1 x 1
theorem add_equiv_class.map_ne_zero_iff {F : Type u_1} {M : Type u_2} {N : Type u_3} [ N] (h : F) {x : M} :
h x 0 x 0
@[protected, instance]
def mul_equiv.has_coe_t {F : Type u_1} {α : Type u_2} {β : Type u_3} [has_mul α] [has_mul β] [ β] :
≃* β)
Equations
@[protected, instance]
def add_equiv.has_coe_t {F : Type u_1} {α : Type u_2} {β : Type u_3} [has_add α] [has_add β] [ β] :
≃+ β)
Equations
@[protected, instance]
def add_equiv.has_coe_to_fun {M : Type u_6} {N : Type u_7} [has_add M] [has_add N] :
has_coe_to_fun (M ≃+ N) (λ (_x : M ≃+ N), M N)
Equations
@[protected, instance]
def mul_equiv.has_coe_to_fun {M : Type u_6} {N : Type u_7} [has_mul M] [has_mul N] :
has_coe_to_fun (M ≃* N) (λ (_x : M ≃* N), M N)
Equations
@[protected, instance]
def mul_equiv.mul_equiv_class {M : Type u_6} {N : Type u_7} [has_mul M] [has_mul N] :
Equations
@[protected, instance]
def add_equiv.add_equiv_class {M : Type u_6} {N : Type u_7} [has_add M] [has_add N] :
Equations
@[simp]
theorem add_equiv.to_equiv_eq_coe {M : Type u_6} {N : Type u_7} [has_add M] [has_add N] (f : M ≃+ N) :
@[simp]
theorem mul_equiv.to_equiv_eq_coe {M : Type u_6} {N : Type u_7} [has_mul M] [has_mul N] (f : M ≃* N) :
@[simp]
theorem mul_equiv.to_fun_eq_coe {M : Type u_6} {N : Type u_7} [has_mul M] [has_mul N] {f : M ≃* N} :
@[simp]
theorem add_equiv.to_fun_eq_coe {M : Type u_6} {N : Type u_7} [has_add M] [has_add N] {f : M ≃+ N} :
@[simp]
theorem mul_equiv.coe_to_equiv {M : Type u_6} {N : Type u_7} [has_mul M] [has_mul N] {f : M ≃* N} :
@[simp]
theorem add_equiv.coe_to_equiv {M : Type u_6} {N : Type u_7} [has_add M] [has_add N] {f : M ≃+ N} :
@[simp]
theorem mul_equiv.coe_to_mul_hom {M : Type u_6} {N : Type u_7} [has_mul M] [has_mul N] {f : M ≃* N} :
@[simp]
theorem add_equiv.coe_to_add_hom {M : Type u_6} {N : Type u_7} [has_add M] [has_add N] {f : M ≃+ N} :
@[protected]
theorem add_equiv.map_add {M : Type u_6} {N : Type u_7} [has_add M] [has_add N] (f : M ≃+ N) (x y : M) :
f (x + y) = f x + f y

@[protected]
theorem mul_equiv.map_mul {M : Type u_6} {N : Type u_7} [has_mul M] [has_mul N] (f : M ≃* N) (x y : M) :
f (x * y) = f x * f y

A multiplicative isomorphism preserves multiplication.

def add_equiv.mk' {M : Type u_6} {N : Type u_7} [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.

Equations
def mul_equiv.mk' {M : Type u_6} {N : Type u_7} [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
@[protected]
theorem add_equiv.bijective {M : Type u_6} {N : Type u_7} [has_add M] [has_add N] (e : M ≃+ N) :
@[protected]
theorem mul_equiv.bijective {M : Type u_6} {N : Type u_7} [has_mul M] [has_mul N] (e : M ≃* N) :
@[protected]
theorem mul_equiv.injective {M : Type u_6} {N : Type u_7} [has_mul M] [has_mul N] (e : M ≃* N) :
@[protected]
theorem add_equiv.injective {M : Type u_6} {N : Type u_7} [has_add M] [has_add N] (e : M ≃+ N) :
@[protected]
theorem mul_equiv.surjective {M : Type u_6} {N : Type u_7} [has_mul M] [has_mul N] (e : M ≃* N) :
@[protected]
theorem add_equiv.surjective {M : Type u_6} {N : Type u_7} [has_add M] [has_add N] (e : M ≃+ N) :
@[refl]
def add_equiv.refl (M : Type u_1) [has_add M] :
M ≃+ M

The identity map is an additive isomorphism.

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

The identity map is a multiplicative isomorphism.

Equations
@[protected, instance]
def add_equiv.inhabited {M : Type u_6} [has_add M] :
Equations
@[protected, instance]
def mul_equiv.inhabited {M : Type u_6} [has_mul M] :
Equations
@[symm]
def add_equiv.symm {M : Type u_6} {N : Type u_7} [has_add M] [has_add N] (h : M ≃+ N) :
N ≃+ M

The inverse of an isomorphism is an isomorphism.

Equations
@[symm]
def mul_equiv.symm {M : Type u_6} {N : Type u_7} [has_mul M] [has_mul N] (h : M ≃* N) :
N ≃* M

The inverse of an isomorphism is an isomorphism.

Equations
@[simp]
theorem mul_equiv.inv_fun_eq_symm {M : Type u_6} {N : Type u_7} [has_mul M] [has_mul N] {f : M ≃* N} :
@[simp]
theorem add_equiv.neg_fun_eq_symm {M : Type u_6} {N : Type u_7} [has_add M] [has_add N] {f : M ≃+ N} :
def add_equiv.simps.symm_apply {M : Type u_6} {N : Type u_7} [has_add M] [has_add N] (e : M ≃+ N) :
N M

See Note custom simps projection

Equations
def mul_equiv.simps.symm_apply {M : Type u_6} {N : Type u_7} [has_mul M] [has_mul N] (e : M ≃* N) :
N M
Equations
@[simp]
theorem mul_equiv.to_equiv_symm {M : Type u_6} {N : Type u_7} [has_mul M] [has_mul N] (f : M ≃* N) :
@[simp]
theorem add_equiv.to_equiv_symm {M : Type u_6} {N : Type u_7} [has_add M] [has_add N] (f : M ≃+ N) :
@[simp]
theorem mul_equiv.coe_mk {M : Type u_6} {N : Type u_7} [has_mul M] [has_mul N] (f : M N) (g : N M) (h₁ : f) (h₂ : 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_6} {N : Type u_7} [has_add M] [has_add N] (f : M N) (g : N M) (h₁ : f) (h₂ : 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 mul_equiv.to_equiv_mk {M : Type u_6} {N : Type u_7} [has_mul M] [has_mul N] (f : M N) (g : N M) (h₁ : f) (h₂ : 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₃}.to_equiv = {to_fun := f, inv_fun := g, left_inv := h₁, right_inv := h₂}
@[simp]
theorem add_equiv.to_equiv_mk {M : Type u_6} {N : Type u_7} [has_add M] [has_add N] (f : M N) (g : N M) (h₁ : f) (h₂ : 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₃}.to_equiv = {to_fun := f, inv_fun := g, left_inv := h₁, right_inv := h₂}
@[simp]
theorem mul_equiv.symm_symm {M : Type u_6} {N : Type u_7} [has_mul M] [has_mul N] (f : M ≃* N) :
f.symm.symm = f
@[simp]
theorem add_equiv.symm_symm {M : Type u_6} {N : Type u_7} [has_add M] [has_add N] (f : M ≃+ N) :
f.symm.symm = f
theorem mul_equiv.symm_bijective {M : Type u_6} {N : Type u_7} [has_mul M] [has_mul N] :
theorem add_equiv.symm_bijective {M : Type u_6} {N : Type u_7} [has_add M] [has_add N] :
@[simp]
theorem mul_equiv.symm_mk {M : Type u_6} {N : Type u_7} [has_mul M] [has_mul N] (f : M N) (g : N M) (h₁ : f) (h₂ : 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 = {to_fun := g, inv_fun := f, left_inv := _, right_inv := _, map_mul' := _}
@[simp]
theorem add_equiv.symm_mk {M : Type u_6} {N : Type u_7} [has_add M] [has_add N] (f : M N) (g : N M) (h₁ : f) (h₂ : 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 = {to_fun := g, inv_fun := f, left_inv := _, right_inv := _, map_add' := _}
@[simp]
theorem add_equiv.refl_symm {M : Type u_6} [has_add M] :
@[simp]
theorem mul_equiv.refl_symm {M : Type u_6} [has_mul M] :
@[trans]
def mul_equiv.trans {M : Type u_6} {N : Type u_7} {P : Type u_8} [has_mul M] [has_mul N] [has_mul P] (h1 : M ≃* N) (h2 : N ≃* P) :
M ≃* P

Transitivity of multiplication-preserving isomorphisms

Equations
@[trans]
def add_equiv.trans {M : Type u_6} {N : Type u_7} {P : Type u_8} [has_add M] [has_add N] [has_add P] (h1 : M ≃+ N) (h2 : N ≃+ P) :
M ≃+ P

Transitivity of addition-preserving isomorphisms

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

`e.symm` is a right inverse of `e`, written as `e (e.symm y) = y`.

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

`e.symm` is a right inverse of `e`, written as `e (e.symm y) = y`.

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

`e.symm` is a left inverse of `e`, written as `e.symm (e y) = y`.

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

`e.symm` is a left inverse of `e`, written as `e.symm (e y) = y`.

@[simp]
theorem mul_equiv.symm_comp_self {M : Type u_6} {N : Type u_7} [has_mul M] [has_mul N] (e : M ≃* N) :
@[simp]
theorem add_equiv.symm_comp_self {M : Type u_6} {N : Type u_7} [has_add M] [has_add N] (e : M ≃+ N) :
@[simp]
theorem add_equiv.self_comp_symm {M : Type u_6} {N : Type u_7} [has_add M] [has_add N] (e : M ≃+ N) :
@[simp]
theorem mul_equiv.self_comp_symm {M : Type u_6} {N : Type u_7} [has_mul M] [has_mul N] (e : M ≃* N) :
@[simp]
theorem mul_equiv.coe_refl {M : Type u_6} [has_mul M] :
@[simp]
theorem add_equiv.coe_refl {M : Type u_6} [has_add M] :
@[simp]
theorem add_equiv.refl_apply {M : Type u_6} [has_add M] (m : M) :
m = m
@[simp]
theorem mul_equiv.refl_apply {M : Type u_6} [has_mul M] (m : M) :
m = m
@[simp]
theorem mul_equiv.coe_trans {M : Type u_6} {N : Type u_7} {P : Type u_8} [has_mul M] [has_mul N] [has_mul P] (e₁ : M ≃* N) (e₂ : N ≃* P) :
(e₁.trans e₂) = e₂ e₁
@[simp]
theorem add_equiv.coe_trans {M : Type u_6} {N : Type u_7} {P : Type u_8} [has_add M] [has_add N] [has_add P] (e₁ : M ≃+ N) (e₂ : N ≃+ P) :
(e₁.trans e₂) = e₂ e₁
@[simp]
theorem mul_equiv.trans_apply {M : Type u_6} {N : Type u_7} {P : Type u_8} [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_6} {N : Type u_7} {P : Type u_8} [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.symm_trans_apply {M : Type u_6} {N : Type u_7} {P : Type u_8} [has_add M] [has_add N] [has_add P] (e₁ : M ≃+ N) (e₂ : N ≃+ P) (p : P) :
((e₁.trans e₂).symm) p = (e₁.symm) ((e₂.symm) p)
@[simp]
theorem mul_equiv.symm_trans_apply {M : Type u_6} {N : Type u_7} {P : Type u_8} [has_mul M] [has_mul N] [has_mul P] (e₁ : M ≃* N) (e₂ : N ≃* P) (p : P) :
((e₁.trans e₂).symm) p = (e₁.symm) ((e₂.symm) p)
@[simp]
theorem add_equiv.apply_eq_iff_eq {M : Type u_6} {N : Type u_7} [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_6} {N : Type u_7} [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_6} {N : Type u_7} [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_6} {N : Type u_7} [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_6} {N : Type u_7} [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_6} {N : Type u_7} [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_6} {N : Type u_7} [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_6} {N : Type u_7} [has_add M] [has_add N] (e : M ≃+ N) {x : N} {y : M} :
y = (e.symm) x e y = x
theorem add_equiv.eq_comp_symm {M : Type u_6} {N : Type u_7} [has_add M] [has_add N] {α : Type u_1} (e : M ≃+ N) (f : N α) (g : M α) :
f = g (e.symm) f e = g
theorem mul_equiv.eq_comp_symm {M : Type u_6} {N : Type u_7} [has_mul M] [has_mul N] {α : Type u_1} (e : M ≃* N) (f : N α) (g : M α) :
f = g (e.symm) f e = g
theorem mul_equiv.comp_symm_eq {M : Type u_6} {N : Type u_7} [has_mul M] [has_mul N] {α : Type u_1} (e : M ≃* N) (f : N α) (g : M α) :
g (e.symm) = f g = f e
theorem add_equiv.comp_symm_eq {M : Type u_6} {N : Type u_7} [has_add M] [has_add N] {α : Type u_1} (e : M ≃+ N) (f : N α) (g : M α) :
g (e.symm) = f g = f e
theorem mul_equiv.eq_symm_comp {M : Type u_6} {N : Type u_7} [has_mul M] [has_mul N] {α : Type u_1} (e : M ≃* N) (f : α M) (g : α N) :
f = (e.symm) g e f = g
theorem add_equiv.eq_symm_comp {M : Type u_6} {N : Type u_7} [has_add M] [has_add N] {α : Type u_1} (e : M ≃+ N) (f : α M) (g : α N) :
f = (e.symm) g e f = g
theorem add_equiv.symm_comp_eq {M : Type u_6} {N : Type u_7} [has_add M] [has_add N] {α : Type u_1} (e : M ≃+ N) (f : α M) (g : α N) :
(e.symm) g = f g = e f
theorem mul_equiv.symm_comp_eq {M : Type u_6} {N : Type u_7} [has_mul M] [has_mul N] {α : Type u_1} (e : M ≃* N) (f : α M) (g : α N) :
(e.symm) g = f g = e f
@[simp]
theorem mul_equiv.symm_trans_self {M : Type u_6} {N : Type u_7} [has_mul M] [has_mul N] (e : M ≃* N) :
e.symm.trans e =
@[simp]
theorem add_equiv.symm_trans_self {M : Type u_6} {N : Type u_7} [has_add M] [has_add N] (e : M ≃+ N) :
e.symm.trans e =
@[simp]
theorem mul_equiv.self_trans_symm {M : Type u_6} {N : Type u_7} [has_mul M] [has_mul N] (e : M ≃* N) :
e.trans e.symm =
@[simp]
theorem add_equiv.self_trans_symm {M : Type u_6} {N : Type u_7} [has_add M] [has_add N] (e : M ≃+ N) :
e.trans e.symm =
@[simp]
theorem add_equiv.coe_add_monoid_hom_refl {M : Type u_1}  :
@[simp]
theorem mul_equiv.coe_monoid_hom_refl {M : Type u_1}  :
@[simp]
theorem add_equiv.coe_add_monoid_hom_trans {M : Type u_1} {N : Type u_2} {P : Type u_3} (e₁ : M ≃+ N) (e₂ : N ≃+ P) :
(e₁.trans e₂) = e₂.comp e₁
@[simp]
theorem mul_equiv.coe_monoid_hom_trans {M : Type u_1} {N : Type u_2} {P : Type u_3} (e₁ : M ≃* N) (e₂ : N ≃* P) :
(e₁.trans e₂) = e₂.comp e₁
@[ext]
theorem add_equiv.ext {M : Type u_6} {N : Type u_7} [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.

@[ext]
theorem mul_equiv.ext {M : Type u_6} {N : Type u_7} [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.

theorem add_equiv.ext_iff {M : Type u_6} {N : Type u_7} [has_add M] [has_add N] {f g : M ≃+ N} :
f = g (x : M), f x = g x
theorem mul_equiv.ext_iff {M : Type u_6} {N : Type u_7} [has_mul M] [has_mul N] {f g : M ≃* N} :
f = g (x : M), f x = g x
@[simp]
theorem mul_equiv.mk_coe {M : Type u_6} {N : Type u_7} [has_mul M] [has_mul N] (e : M ≃* N) (e' : N M) (h₁ : e) (h₂ : e) (h₃ : (x y : M), e (x * y) = e x * e y) :
{to_fun := e, inv_fun := e', left_inv := h₁, right_inv := h₂, map_mul' := h₃} = e
@[simp]
theorem add_equiv.mk_coe {M : Type u_6} {N : Type u_7} [has_add M] [has_add N] (e : M ≃+ N) (e' : N M) (h₁ : e) (h₂ : e) (h₃ : (x y : M), e (x + y) = e x + e y) :
{to_fun := e, inv_fun := e', left_inv := h₁, right_inv := h₂, map_add' := h₃} = e
@[simp]
theorem mul_equiv.mk_coe' {M : Type u_6} {N : Type u_7} [has_mul M] [has_mul N] (e : M ≃* N) (f : N M) (h₁ : f) (h₂ : f) (h₃ : (x y : N), f (x * y) = f x * f y) :
{to_fun := f, inv_fun := e, left_inv := h₁, right_inv := h₂, map_mul' := h₃} = e.symm
@[simp]
theorem add_equiv.mk_coe' {M : Type u_6} {N : Type u_7} [has_add M] [has_add N] (e : M ≃+ N) (f : N M) (h₁ : f) (h₂ : f) (h₃ : (x y : N), f (x + y) = f x + f y) :
{to_fun := f, inv_fun := e, left_inv := h₁, right_inv := h₂, map_add' := h₃} = e.symm
@[protected]
theorem add_equiv.congr_arg {M : Type u_6} {N : Type u_7} [has_add M] [has_add N] {f : M ≃+ N} {x x' : M} :
x = x' f x = f x'
@[protected]
theorem mul_equiv.congr_arg {M : Type u_6} {N : Type u_7} [has_mul M] [has_mul N] {f : M ≃* N} {x x' : M} :
x = x' f x = f x'
@[protected]
theorem add_equiv.congr_fun {M : Type u_6} {N : Type u_7} [has_add M] [has_add N] {f g : M ≃+ N} (h : f = g) (x : M) :
f x = g x
@[protected]
theorem mul_equiv.congr_fun {M : Type u_6} {N : Type u_7} [has_mul M] [has_mul N] {f g : M ≃* N} (h : f = g) (x : M) :
f x = g x
def add_equiv.add_equiv_of_unique {M : Type u_1} {N : Type u_2} [unique M] [unique N] [has_add M] [has_add N] :
M ≃+ N

The `add_equiv` between two add_monoids with a unique element.

Equations
def mul_equiv.mul_equiv_of_unique {M : Type u_1} {N : Type u_2} [unique M] [unique N] [has_mul M] [has_mul N] :
M ≃* N

The `mul_equiv` between two monoids with a unique element.

Equations
@[protected, instance]
def add_equiv.unique {M : Type u_1} {N : Type u_2} [unique M] [unique N] [has_add M] [has_add N] :
unique (M ≃+ N)

There is a unique additive monoid homomorphism between two additive monoids with a unique element.

Equations
@[protected, instance]
def mul_equiv.unique {M : Type u_1} {N : Type u_2} [unique M] [unique N] [has_mul M] [has_mul N] :
unique (M ≃* N)

There is a unique monoid homomorphism between two monoids with a unique element.

Equations

## Monoids #

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

An additive isomorphism of additive monoids sends `0` to `0` (and is hence an additive monoid isomorphism).

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

A multiplicative isomorphism of monoids sends `1` to `1` (and is hence a monoid isomorphism).

@[protected]
theorem add_equiv.map_eq_zero_iff {M : Type u_1} {N : Type u_2} (h : M ≃+ N) {x : M} :
h x = 0 x = 0
@[protected]
theorem mul_equiv.map_eq_one_iff {M : Type u_1} {N : Type u_2} (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} (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} (h : M ≃* N) {x : M} :
h x 1 x 1
noncomputable def add_equiv.of_bijective {M : Type u_1} {N : Type u_2} {F : Type u_3} [has_add M] [has_add N] [ N] (f : F) (hf : function.bijective f) :
M ≃+ N

A bijective `add_semigroup` homomorphism is an isomorphism

Equations
@[simp]
theorem add_equiv.of_bijective_apply {M : Type u_1} {N : Type u_2} {F : Type u_3} [has_add M] [has_add N] [ N] (f : F) (hf : function.bijective f) (ᾰ : M) :
hf) = hf).to_fun
noncomputable def mul_equiv.of_bijective {M : Type u_1} {N : Type u_2} {F : Type u_3} [has_mul M] [has_mul N] [ N] (f : F) (hf : function.bijective f) :
M ≃* N

A bijective `semigroup` homomorphism is an isomorphism

Equations
@[simp]
theorem mul_equiv.of_bijective_apply {M : Type u_1} {N : Type u_2} {F : Type u_3} [has_mul M] [has_mul N] [ N] (f : F) (hf : function.bijective f) (ᾰ : M) :
hf) = hf).to_fun
@[simp]
theorem mul_equiv.of_bijective_apply_symm_apply {M : Type u_1} {N : Type u_2} {n : N} (f : M →* N) (hf : function.bijective f) :
f ( hf).symm) n) = n
def add_equiv.to_add_monoid_hom {M : Type u_1} {N : Type u_2} (h : M ≃+ N) :
M →+ N

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

Equations
def mul_equiv.to_monoid_hom {M : Type u_1} {N : Type u_2} (h : M ≃* N) :
M →* 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} (e : M ≃* N) :
@[simp]
theorem add_equiv.coe_to_add_monoid_hom {M : Type u_1} {N : Type u_2} (e : M ≃+ N) :
theorem mul_equiv.to_monoid_hom_injective {M : Type u_1} {N : Type u_2}  :
theorem add_equiv.to_add_monoid_hom_injective {M : Type u_1} {N : Type u_2}  :
@[simp]
theorem add_equiv.arrow_congr_apply {M : Type u_1} {N : Type u_2} {P : Type u_3} {Q : Type u_4} [has_add P] [has_add Q] (f : M N) (g : P ≃+ Q) (h : M P) (n : N) :
h n = g (h ((f.symm) n))
def add_equiv.arrow_congr {M : Type u_1} {N : Type u_2} {P : Type u_3} {Q : Type u_4} [has_add P] [has_add Q] (f : M N) (g : P ≃+ Q) :
(M P) ≃+ (N Q)

An additive analogue of `equiv.arrow_congr`, where the equivalence between the targets is additive.

Equations
def mul_equiv.arrow_congr {M : Type u_1} {N : Type u_2} {P : Type u_3} {Q : Type u_4} [has_mul P] [has_mul Q] (f : M N) (g : P ≃* Q) :
(M P) ≃* (N Q)

A multiplicative analogue of `equiv.arrow_congr`, where the equivalence between the targets is multiplicative.

Equations
@[simp]
theorem mul_equiv.arrow_congr_apply {M : Type u_1} {N : Type u_2} {P : Type u_3} {Q : Type u_4} [has_mul P] [has_mul Q] (f : M N) (g : P ≃* Q) (h : M P) (n : N) :
h n = g (h ((f.symm) n))
def add_equiv.add_monoid_hom_congr {M : Type u_1} {N : Type u_2} {P : Type u_3} {Q : Type u_4} (f : M ≃+ N) (g : P ≃+ Q) :
(M →+ P) ≃+ (N →+ Q)

An additive analogue of `equiv.arrow_congr`, for additive maps from an additive monoid to a commutative additive monoid.

Equations
@[simp]
theorem add_equiv.add_monoid_hom_congr_apply {M : Type u_1} {N : Type u_2} {P : Type u_3} {Q : Type u_4} (f : M ≃+ N) (g : P ≃+ Q) (h : M →+ P) :
def mul_equiv.monoid_hom_congr {M : Type u_1} {N : Type u_2} {P : Type u_3} {Q : Type u_4} [comm_monoid P] [comm_monoid Q] (f : M ≃* N) (g : P ≃* Q) :
(M →* P) ≃* (N →* Q)

A multiplicative analogue of `equiv.arrow_congr`, for multiplicative maps from a monoid to a commutative monoid.

Equations
@[simp]
theorem mul_equiv.monoid_hom_congr_apply {M : Type u_1} {N : Type u_2} {P : Type u_3} {Q : Type u_4} [comm_monoid P] [comm_monoid Q] (f : M ≃* N) (g : P ≃* Q) (h : M →* P) :
@[simp]
theorem mul_equiv.Pi_congr_right_apply {η : Type u_1} {Ms : η Type u_2} {Ns : η Type u_3} [Π (j : η), has_mul (Ms j)] [Π (j : η), has_mul (Ns j)] (es : Π (j : η), Ms j ≃* Ns j) (x : Π (j : η), Ms j) (j : η) :
j = (es j) (x j)
@[simp]
theorem add_equiv.Pi_congr_right_apply {η : Type u_1} {Ms : η Type u_2} {Ns : η Type u_3} [Π (j : η), has_add (Ms j)] [Π (j : η), has_add (Ns j)] (es : Π (j : η), Ms j ≃+ Ns j) (x : Π (j : η), Ms j) (j : η) :
j = (es j) (x j)
def add_equiv.Pi_congr_right {η : Type u_1} {Ms : η Type u_2} {Ns : η Type u_3} [Π (j : η), has_add (Ms j)] [Π (j : η), has_add (Ns j)] (es : Π (j : η), Ms j ≃+ Ns j) :
(Π (j : η), Ms j) ≃+ Π (j : η), Ns j

A family of additive equivalences `Π j, (Ms j ≃+ Ns j)` generates an additive equivalence between `Π j, Ms j` and `Π j, Ns j`.

This is the `add_equiv` version of `equiv.Pi_congr_right`, and the dependent version of `add_equiv.arrow_congr`.

Equations
def mul_equiv.Pi_congr_right {η : Type u_1} {Ms : η Type u_2} {Ns : η Type u_3} [Π (j : η), has_mul (Ms j)] [Π (j : η), has_mul (Ns j)] (es : Π (j : η), Ms j ≃* Ns j) :
(Π (j : η), Ms j) ≃* Π (j : η), Ns j

A family of multiplicative equivalences `Π j, (Ms j ≃* Ns j)` generates a multiplicative equivalence between `Π j, Ms j` and `Π j, Ns j`.

This is the `mul_equiv` version of `equiv.Pi_congr_right`, and the dependent version of `mul_equiv.arrow_congr`.

Equations
@[simp]
theorem mul_equiv.Pi_congr_right_refl {η : Type u_1} {Ms : η Type u_2} [Π (j : η), has_mul (Ms j)] :
mul_equiv.Pi_congr_right (λ (j : η), mul_equiv.refl (Ms j)) = mul_equiv.refl (Π (j : η), Ms j)
@[simp]
theorem add_equiv.Pi_congr_right_refl {η : Type u_1} {Ms : η Type u_2} [Π (j : η), has_add (Ms j)] :
add_equiv.Pi_congr_right (λ (j : η), add_equiv.refl (Ms j)) = add_equiv.refl (Π (j : η), Ms j)
@[simp]
theorem mul_equiv.Pi_congr_right_symm {η : Type u_1} {Ms : η Type u_2} {Ns : η Type u_3} [Π (j : η), has_mul (Ms j)] [Π (j : η), has_mul (Ns j)] (es : Π (j : η), Ms j ≃* Ns j) :
= mul_equiv.Pi_congr_right (λ (i : η), (es i).symm)
@[simp]
theorem add_equiv.Pi_congr_right_symm {η : Type u_1} {Ms : η Type u_2} {Ns : η Type u_3} [Π (j : η), has_add (Ms j)] [Π (j : η), has_add (Ns j)] (es : Π (j : η), Ms j ≃+ Ns j) :
= add_equiv.Pi_congr_right (λ (i : η), (es i).symm)
@[simp]
theorem mul_equiv.Pi_congr_right_trans {η : Type u_1} {Ms : η Type u_2} {Ns : η Type u_3} {Ps : η Type u_4} [Π (j : η), has_mul (Ms j)] [Π (j : η), has_mul (Ns j)] [Π (j : η), has_mul (Ps j)] (es : Π (j : η), Ms j ≃* Ns j) (fs : Π (j : η), Ns j ≃* Ps j) :
= mul_equiv.Pi_congr_right (λ (i : η), (es i).trans (fs i))
@[simp]
theorem add_equiv.Pi_congr_right_trans {η : Type u_1} {Ms : η Type u_2} {Ns : η Type u_3} {Ps : η Type u_4} [Π (j : η), has_add (Ms j)] [Π (j : η), has_add (Ns j)] [Π (j : η), has_add (Ps j)] (es : Π (j : η), Ms j ≃+ Ns j) (fs : Π (j : η), Ns j ≃+ Ps j) :
= add_equiv.Pi_congr_right (λ (i : η), (es i).trans (fs i))
@[simp]
theorem mul_equiv.Pi_subsingleton_apply {ι : Type u_1} (M : ι Type u_2) [Π (j : ι), has_mul (M j)] [subsingleton ι] (i : ι) (ᾰ : Π (a' : ι), M a') :
= .to_fun
@[simp]
theorem mul_equiv.Pi_subsingleton_symm_apply {ι : Type u_1} (M : ι Type u_2) [Π (j : ι), has_mul (M j)] [subsingleton ι] (i : ι) (ᾰ : M i) (a' : ι) :
.symm) a' = .inv_fun a'
def mul_equiv.Pi_subsingleton {ι : Type u_1} (M : ι Type u_2) [Π (j : ι), has_mul (M j)] [subsingleton ι] (i : ι) :
(Π (j : ι), M j) ≃* M i

A family indexed by a nonempty subsingleton type is equivalent to the element at the single index.

Equations
def add_equiv.Pi_subsingleton {ι : Type u_1} (M : ι Type u_2) [Π (j : ι), has_add (M j)] [subsingleton ι] (i : ι) :
(Π (j : ι), M j) ≃+ M i

A family indexed by a nonempty subsingleton type is equivalent to the element at the single index.

Equations
@[simp]
theorem add_equiv.Pi_subsingleton_apply {ι : Type u_1} (M : ι Type u_2) [Π (j : ι), has_add (M j)] [subsingleton ι] (i : ι) (ᾰ : Π (a' : ι), M a') :
= .to_fun
@[simp]
theorem add_equiv.Pi_subsingleton_symm_apply {ι : Type u_1} (M : ι Type u_2) [Π (j : ι), has_add (M j)] [subsingleton ι] (i : ι) (ᾰ : M i) (a' : ι) :
.symm) a' = .inv_fun a'

# Groups #

@[protected]
theorem add_equiv.map_neg {G : Type u_10} {H : Type u_11} [add_group G] (h : G ≃+ H) (x : G) :
h (-x) = -h x

An additive equivalence of additive groups preserves negation.

@[protected]
theorem mul_equiv.map_inv {G : Type u_10} {H : Type u_11} [group G] (h : G ≃* H) (x : G) :

A multiplicative equivalence of groups preserves inversion.

@[protected]
theorem add_equiv.map_sub {G : Type u_10} {H : Type u_11} [add_group G] (h : G ≃+ H) (x y : G) :
h (x - y) = h x - h y

An additive equivalence of additive groups preserves subtractions.

@[protected]
theorem mul_equiv.map_div {G : Type u_10} {H : Type u_11} [group G] (h : G ≃* H) (x y : G) :
h (x / y) = h x / h y

A multiplicative equivalence of groups preserves division.

@[simp]
theorem add_hom.to_add_equiv_symm_apply {M : Type u_6} {N : Type u_7} [has_add M] [has_add N] (f : N) (g : M) (h₁ : g.comp f = ) (h₂ : f.comp g = ) :
((f.to_add_equiv g h₁ h₂).symm) = g
@[simp]
theorem mul_hom.to_mul_equiv_symm_apply {M : Type u_6} {N : Type u_7} [has_mul M] [has_mul N] (f : M →ₙ* N) (g : N →ₙ* M) (h₁ : g.comp f = ) (h₂ : f.comp g = ) :
((f.to_mul_equiv g h₁ h₂).symm) = g
def add_hom.to_add_equiv {M : Type u_6} {N : Type u_7} [has_add M] [has_add N] (f : N) (g : M) (h₁ : g.comp f = ) (h₂ : f.comp g = ) :
M ≃+ N

Given a pair of additive 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 homomorphisms.

Equations
def mul_hom.to_mul_equiv {M : Type u_6} {N : Type u_7} [has_mul M] [has_mul N] (f : M →ₙ* N) (g : N →ₙ* M) (h₁ : g.comp f = ) (h₂ : f.comp g = ) :
M ≃* N

Given a pair of multiplicative 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 multiplicative homomorphisms.

Equations
@[simp]
theorem mul_hom.to_mul_equiv_apply {M : Type u_6} {N : Type u_7} [has_mul M] [has_mul N] (f : M →ₙ* N) (g : N →ₙ* M) (h₁ : g.comp f = ) (h₂ : f.comp g = ) :
(f.to_mul_equiv g h₁ h₂) = f
@[simp]
theorem add_hom.to_add_equiv_apply {M : Type u_6} {N : Type u_7} [has_add M] [has_add N] (f : N) (g : M) (h₁ : g.comp f = ) (h₂ : f.comp g = ) :
(f.to_add_equiv g h₁ h₂) = f
def add_monoid_hom.to_add_equiv {M : Type u_6} {N : Type u_7} (f : M →+ N) (g : N →+ M) (h₁ : g.comp f = ) (h₂ : f.comp g = ) :
M ≃+ N

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
@[simp]
theorem monoid_hom.to_mul_equiv_apply {M : Type u_6} {N : Type u_7} (f : M →* N) (g : N →* M) (h₁ : g.comp f = ) (h₂ : f.comp g = ) :
(f.to_mul_equiv g h₁ h₂) = f
def monoid_hom.to_mul_equiv {M : Type u_6} {N : Type u_7} (f : M →* N) (g : N →* M) (h₁ : g.comp f = ) (h₂ : f.comp g = ) :
M ≃* 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.to_add_equiv_symm_apply {M : Type u_6} {N : Type u_7} (f : M →+ N) (g : N →+ M) (h₁ : g.comp f = ) (h₂ : f.comp g = ) :
((f.to_add_equiv g h₁ h₂).symm) = g
@[simp]
theorem add_monoid_hom.to_add_equiv_apply {M : Type u_6} {N : Type u_7} (f : M →+ N) (g : N →+ M) (h₁ : g.comp f = ) (h₂ : f.comp g = ) :
(f.to_add_equiv g h₁ h₂) = f
@[simp]
theorem monoid_hom.to_mul_equiv_symm_apply {M : Type u_6} {N : Type u_7} (f : M →* N) (g : N →* M) (h₁ : g.comp f = ) (h₂ : f.comp g = ) :
((f.to_mul_equiv g h₁ h₂).symm) = g
@[simp]
theorem equiv.neg_apply (G : Type u_10)  :
@[protected]
def equiv.neg (G : Type u_10)  :

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

Equations
@[simp]
theorem equiv.inv_apply (G : Type u_10)  :
@[protected]
def equiv.inv (G : Type u_10)  :

Inversion on a `group` or `group_with_zero` is a permutation of the underlying type.

Equations
@[simp]
theorem equiv.neg_symm {G : Type u_10}  :
@[simp]
theorem equiv.inv_symm {G : Type u_10}  :