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.

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.

Tags #

equiv, mul_equiv, add_equiv

source
def add_hom.inverse {M : Type u_3} {N : Type u_4} [has_add M] [has_add N] (f : add_hom M N) (g : N → M) (h₁ : function.left_inverse g ⇑f) (h₂ : function.right_inverse g ⇑f) :
add_hom N M

Makes an additive inverse from a bijection which preserves addition.

source
def mul_hom.inverse {M : Type u_3} {N : Type u_4} [has_mul M] [has_mul N] (f : mul_hom M N) (g : N → M) (h₁ : function.left_inverse g ⇑f) (h₂ : function.right_inverse g ⇑f) :
mul_hom N M

Makes a multiplicative inverse from a bijection which preserves multiplication.

Equations
source
def add_equiv.to_equiv {A : Type u_9} {B : Type u_10} [has_add A] [has_add B] (self : A ≃+ B) :
A ≃ B

The equiv underlying an add_equiv.

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

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

source
def add_equiv.to_add_hom {A : Type u_9} {B : Type u_10} [has_add A] [has_add B] (self : A ≃+ B) :
add_hom A B

The add_hom underlying a add_equiv.

source
def mul_equiv.to_mul_hom {M : Type u_9} {N : Type u_10} [has_mul M] [has_mul N] (self : M ≃* N) :
mul_hom M N

The mul_hom underlying a mul_equiv.

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

The equiv underlying a mul_equiv.

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

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

source
@[protected, 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
@[protected, 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_eq_coe {M : Type u_3} {N : Type u_4} [has_mul M] [has_mul N] {f : M ≃* N} :
f.to_fun = ⇑f
source
@[simp]
theorem add_equiv.to_fun_eq_coe {M : Type u_3} {N : Type u_4} [has_add M] [has_add N] {f : M ≃+ N} :
f.to_fun = ⇑f
source
@[simp]
theorem mul_equiv.coe_to_equiv {M : Type u_3} {N : Type u_4} [has_mul M] [has_mul N] {f : M ≃* N} :
⇑(f.to_equiv) = ⇑f
source
@[simp]
theorem add_equiv.coe_to_equiv {M : Type u_3} {N : Type u_4} [has_add M] [has_add N] {f : M ≃+ N} :
⇑(f.to_equiv) = ⇑f
source
@[simp]
theorem mul_equiv.coe_to_mul_hom {M : Type u_3} {N : Type u_4} [has_mul M] [has_mul N] {f : M ≃* N} :
⇑(f.to_mul_hom) = ⇑f
source
@[simp]
theorem add_equiv.coe_to_add_hom {M : Type u_3} {N : Type u_4} [has_add M] [has_add N] {f : M ≃+ N} :
⇑(f.to_add_hom) = ⇑f
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
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
@[protected]
theorem add_equiv.bijective {M : Type u_3} {N : Type u_4} [has_add M] [has_add N] (e : M ≃+ N) :
function.bijective ⇑e
source
@[protected]
theorem mul_equiv.bijective {M : Type u_3} {N : Type u_4} [has_mul M] [has_mul N] (e : M ≃* N) :
function.bijective ⇑e
source
@[protected]
theorem mul_equiv.injective {M : Type u_3} {N : Type u_4} [has_mul M] [has_mul N] (e : M ≃* N) :
function.injective ⇑e
source
@[protected]
theorem add_equiv.injective {M : Type u_3} {N : Type u_4} [has_add M] [has_add N] (e : M ≃+ N) :
function.injective ⇑e
source
@[protected]
theorem mul_equiv.surjective {M : Type u_3} {N : Type u_4} [has_mul M] [has_mul N] (e : M ≃* N) :
function.surjective ⇑e
source
@[protected]
theorem add_equiv.surjective {M : Type u_3} {N : Type u_4} [has_add M] [has_add N] (e : M ≃+ N) :
function.surjective ⇑e
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
@[protected, instance]
def add_equiv.inhabited {M : Type u_3} [has_add M] :
inhabited (M ≃+ M)
source
@[protected, 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
def add_equiv.simps.symm_apply {M : Type u_3} {N : Type u_4} [has_add M] [has_add N] (e : M ≃+ N) :
N → M

See Note custom simps projection

source
def mul_equiv.simps.symm_apply {M : Type u_3} {N : Type u_4} [has_mul M] [has_mul N] (e : M ≃* N) :
N → M

See Note [custom simps projection]

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 mul_equiv.symm_symm {M : Type u_3} {N : Type u_4} [has_mul M] [has_mul N] (f : M ≃* N) :
f.symm.symm = f
source
@[simp]
theorem add_equiv.symm_symm {M : Type u_3} {N : Type u_4} [has_add M] [has_add N] (f : M ≃+ N) :
f.symm.symm = f
source
theorem mul_equiv.symm_bijective {M : Type u_3} {N : Type u_4} [has_mul M] [has_mul N] :
function.bijective mul_equiv.symm
source
theorem add_equiv.symm_bijective {M : Type u_3} {N : Type u_4} [has_add M] [has_add N] :
function.bijective add_equiv.symm
source
@[simp]
theorem mul_equiv.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 = {to_fun := g, inv_fun := f, left_inv := _, right_inv := _, map_mul' := _}
source
@[simp]
theorem add_equiv.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 = {to_fun := g, inv_fun := f, left_inv := _, right_inv := _, map_add' := _}
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 mul_equiv.symm_comp_self {M : Type u_3} {N : Type u_4} [has_mul M] [has_mul N] (e : M ≃* N) :
⇑(e.symm) ∘ ⇑e = id
source
@[simp]
theorem add_equiv.symm_comp_self {M : Type u_3} {N : Type u_4} [has_add M] [has_add N] (e : M ≃+ N) :
⇑(e.symm) ∘ ⇑e = id
source
@[simp]
theorem add_equiv.self_comp_symm {M : Type u_3} {N : Type u_4} [has_add M] [has_add N] (e : M ≃+ N) :
⇑e ∘ ⇑(e.symm) = id
source
@[simp]
theorem mul_equiv.self_comp_symm {M : Type u_3} {N : Type u_4} [has_mul M] [has_mul N] (e : M ≃* N) :
⇑e ∘ ⇑(e.symm) = id
source
@[simp]
theorem mul_equiv.coe_refl {M : Type u_3} [has_mul M] :
⇑(mul_equiv.refl M) = id
source
@[simp]
theorem add_equiv.coe_refl {M : Type u_3} [has_add M] :
⇑(add_equiv.refl M) = id
source
theorem add_equiv.refl_apply {M : Type u_3} [has_add M] (m : M) :
⇑(add_equiv.refl M) m = m
source
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.coe_trans {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) :
⇑(e₁.trans e₂) = ⇑e₂ ∘ ⇑e₁
source
@[simp]
theorem add_equiv.coe_trans {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) :
⇑(e₁.trans e₂) = ⇑e₂ ∘ ⇑e₁
source
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
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.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
source
@[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
source
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
source
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
source
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
source
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
source
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
source
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
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.ext_iff {M : Type u_3} {N : Type u_4} [has_add M] [has_add N] {f g : M ≃+ N} :
f = g ↔ ∀ (x : M), ⇑f x = ⇑g x
source
theorem mul_equiv.ext_iff {M : Type u_3} {N : Type u_4} [has_mul M] [has_mul N] {f g : M ≃* N} :
f = g ↔ ∀ (x : M), ⇑f x = ⇑g x
source
@[simp]
theorem mul_equiv.mk_coe {M : Type u_3} {N : Type u_4} [has_mul M] [has_mul N] (e : M ≃* N) (e' : N → M) (h₁ : function.left_inverse e' ⇑e) (h₂ : function.right_inverse e' ⇑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
source
@[simp]
theorem add_equiv.mk_coe {M : Type u_3} {N : Type u_4} [has_add M] [has_add N] (e : M ≃+ N) (e' : N → M) (h₁ : function.left_inverse e' ⇑e) (h₂ : function.right_inverse e' ⇑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
source
@[simp]
theorem mul_equiv.mk_coe' {M : Type u_3} {N : Type u_4} [has_mul M] [has_mul N] (e : M ≃* N) (f : N → M) (h₁ : function.left_inverse ⇑e f) (h₂ : function.right_inverse ⇑e 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
source
@[simp]
theorem add_equiv.mk_coe' {M : Type u_3} {N : Type u_4} [has_add M] [has_add N] (e : M ≃+ N) (f : N → M) (h₁ : function.left_inverse ⇑e f) (h₂ : function.right_inverse ⇑e 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
source
@[protected]
theorem add_equiv.congr_arg {M : Type u_3} {N : Type u_4} [has_add M] [has_add N] {f : M ≃+ N} {x x' : M} :
x = x' → ⇑f x = ⇑f x'
source
@[protected]
theorem mul_equiv.congr_arg {M : Type u_3} {N : Type u_4} [has_mul M] [has_mul N] {f : M ≃* N} {x x' : M} :
x = x' → ⇑f x = ⇑f x'
source
@[protected]
theorem add_equiv.congr_fun {M : Type u_3} {N : Type u_4} [has_add M] [has_add N] {f g : M ≃+ N} (h : f = g) (x : M) :
⇑f x = ⇑g x
source
@[protected]
theorem mul_equiv.congr_fun {M : Type u_3} {N : Type u_4} [has_mul M] [has_mul N] {f g : M ≃* N} (h : f = g) (x : M) :
⇑f x = ⇑g x
source
def add_equiv.add_equiv_of_unique_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.

source
def mul_equiv.mul_equiv_of_unique_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
source
@[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)
source
@[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 #

source
@[simp]
theorem add_equiv.map_zero {M : Type u_1} {N : Type u_2} [add_zero_class M] [add_zero_class N] (h : M ≃+ N) :
⇑h 0 = 0
source
@[simp]
theorem mul_equiv.map_one {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class 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_zero_class M] [add_zero_class 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} [mul_one_class M] [mul_one_class 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_zero_class M] [add_zero_class 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} [mul_one_class M] [mul_one_class 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_zero_class M] [add_zero_class 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} [mul_one_class M] [mul_one_class 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_zero_class M] [add_zero_class 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} [mul_one_class M] [mul_one_class N] (h : M ≃* N) :
M →* N

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

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

source
def mul_equiv.arrow_congr {M : Type u_1} {N : Type u_2} {P : Type u_3} {Q : Type u_4} [mul_one_class P] [mul_one_class 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
source
@[simp]
theorem mul_equiv.arrow_congr_apply {M : Type u_1} {N : Type u_2} {P : Type u_3} {Q : Type u_4} [mul_one_class P] [mul_one_class Q] (f : M ≃ N) (g : P ≃* Q) (h : M → P) (n : N) :
⇑(mul_equiv.arrow_congr f g) h n = ⇑g (h (⇑(f.symm) n))
source
def add_equiv.add_monoid_hom_congr {M : Type u_1} {N : Type u_2} {P : Type u_3} {Q : Type u_4} [add_zero_class M] [add_zero_class N] [add_comm_monoid P] [add_comm_monoid Q] (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.

source
@[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} [add_zero_class M] [add_zero_class N] [add_comm_monoid P] [add_comm_monoid Q] (f : M ≃+ N) (g : P ≃+ Q) (h : M →+ P) :
⇑(f.add_monoid_hom_congr g) h = g.to_add_monoid_hom.comp (h.comp f.symm.to_add_monoid_hom)
source
def mul_equiv.monoid_hom_congr {M : Type u_1} {N : Type u_2} {P : Type u_3} {Q : Type u_4} [mul_one_class M] [mul_one_class N] [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
source
@[simp]
theorem mul_equiv.monoid_hom_congr_apply {M : Type u_1} {N : Type u_2} {P : Type u_3} {Q : Type u_4} [mul_one_class M] [mul_one_class N] [comm_monoid P] [comm_monoid Q] (f : M ≃* N) (g : P ≃* Q) (h : M →* P) :
⇑(f.monoid_hom_congr g) h = g.to_monoid_hom.comp (h.comp f.symm.to_monoid_hom)
source
@[simp]
theorem mul_equiv.Pi_congr_right_apply {η : Type u_1} {Ms : η → Type u_2} {Ns : η → Type u_3} [Π (j : η), mul_one_class (Ms j)] [Π (j : η), mul_one_class (Ns j)] (es : Π (j : η), Ms j ≃* Ns j) (x : Π (j : η), Ms j) (j : η) :
⇑(mul_equiv.Pi_congr_right es) x j = ⇑(es j) (x j)
source
@[simp]
theorem add_equiv.Pi_congr_right_apply {η : Type u_1} {Ms : η → Type u_2} {Ns : η → Type u_3} [Π (j : η), add_zero_class (Ms j)] [Π (j : η), add_zero_class (Ns j)] (es : Π (j : η), Ms j ≃+ Ns j) (x : Π (j : η), Ms j) (j : η) :
⇑(add_equiv.Pi_congr_right es) x j = ⇑(es j) (x j)
source
def add_equiv.Pi_congr_right {η : Type u_1} {Ms : η → Type u_2} {Ns : η → Type u_3} [Π (j : η), add_zero_class (Ms j)] [Π (j : η), add_zero_class (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.

source
def mul_equiv.Pi_congr_right {η : Type u_1} {Ms : η → Type u_2} {Ns : η → Type u_3} [Π (j : η), mul_one_class (Ms j)] [Π (j : η), mul_one_class (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
source
@[simp]
theorem mul_equiv.Pi_congr_right_refl {η : Type u_1} {Ms : η → Type u_2} [Π (j : η), mul_one_class (Ms j)] :
mul_equiv.Pi_congr_right (λ (j : η), mul_equiv.refl (Ms j)) = mul_equiv.refl (Π (j : η), Ms j)
source
@[simp]
theorem mul_equiv.Pi_congr_right_symm {η : Type u_1} {Ms : η → Type u_2} {Ns : η → Type u_3} [Π (j : η), mul_one_class (Ms j)] [Π (j : η), mul_one_class (Ns j)] (es : Π (j : η), Ms j ≃* Ns j) :
(mul_equiv.Pi_congr_right es).symm = mul_equiv.Pi_congr_right (λ (i : η), (es i).symm)
source
@[simp]
theorem mul_equiv.Pi_congr_right_trans {η : Type u_1} {Ms : η → Type u_2} {Ns : η → Type u_3} {Ps : η → Type u_4} [Π (j : η), mul_one_class (Ms j)] [Π (j : η), mul_one_class (Ns j)] [Π (j : η), mul_one_class (Ps j)] (es : Π (j : η), Ms j ≃* Ns j) (fs : Π (j : η), Ns j ≃* Ps j) :
(mul_equiv.Pi_congr_right es).trans (mul_equiv.Pi_congr_right fs) = mul_equiv.Pi_congr_right (λ (i : η), (es i).trans (fs i))

Groups #

source
@[simp]
theorem add_equiv.map_neg {G : Type u_7} {H : Type u_8} [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_7} {H : Type u_8} [group G] [group H] (h : G ≃* H) (x : G) :
⇑h x⁻¹ = (⇑h x)⁻¹

A multiplicative equivalence of groups preserves inversion.

source
def add_monoid_hom.to_add_equiv {M : Type u_3} {N : Type u_4} [add_zero_class M] [add_zero_class 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) :
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
source
@[simp]
theorem monoid_hom.to_mul_equiv_apply {M : Type u_3} {N : Type u_4} [mul_one_class M] [mul_one_class 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
source
def monoid_hom.to_mul_equiv {M : Type u_3} {N : Type u_4} [mul_one_class M] [mul_one_class N] (f : M →* N) (g : N →* M) (h₁ : g.comp f = monoid_hom.id M) (h₂ : f.comp g = monoid_hom.id N) :
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
source
@[simp]
theorem add_monoid_hom.to_add_equiv_symm_apply {M : Type u_3} {N : Type u_4} [add_zero_class M] [add_zero_class 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₂).symm) = ⇑g
source
@[simp]
theorem add_monoid_hom.to_add_equiv_apply {M : Type u_3} {N : Type u_4} [add_zero_class M] [add_zero_class 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
source
@[simp]
theorem monoid_hom.to_mul_equiv_symm_apply {M : Type u_3} {N : Type u_4} [mul_one_class M] [mul_one_class 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₂).symm) = ⇑g
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
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
@[protected]
theorem group.is_unit {G : Type u_1} [group G] (x : G) :
is_unit x
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
@[simp]
theorem add_units.add_left_apply {M : Type u_3} [add_monoid M] (u : add_units M) :
⇑(u.add_left) = λ (x : M), ↑u + x
source
@[simp]
theorem units.mul_left_apply {M : Type u_3} [monoid M] (u : units M) :
⇑(u.mul_left) = λ (x : M), (↑u) * x
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.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
@[simp]
theorem units.mul_right_apply {M : Type u_3} [monoid M] (u : units M) :
⇑(u.mul_right) = λ (x : M), x * ↑u
source
@[simp]
theorem add_units.add_right_apply {M : Type u_3} [add_monoid M] (u : add_units M) :
⇑(u.add_right) = λ (x : M), x + ↑u
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 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
@[protected]
def equiv.add_left {G : Type u_7} [add_group G] (a : G) :
equiv.perm G

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

source
@[protected]
def equiv.mul_left {G : Type u_7} [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_7} [group G] (a : G) :
⇑(equiv.mul_left a) = has_mul.mul a
source
@[simp]
theorem equiv.coe_add_left {G : Type u_7} [add_group G] (a : G) :
⇑(equiv.add_left a) = has_add.add a
source
@[simp, nolint]
theorem equiv.add_left_symm_apply {G : Type u_7} [add_group G] (a : G) :
⇑(equiv.symm (equiv.add_left a)) = has_add.add (-a)
source
@[simp, nolint]
theorem equiv.mul_left_symm_apply {G : Type u_7} [group G] (a : G) :
⇑(equiv.symm (equiv.mul_left a)) = has_mul.mul a⁻¹

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

source
@[simp]
theorem equiv.mul_left_symm {G : Type u_7} [group G] (a : G) :
equiv.symm (equiv.mul_left a) = equiv.mul_left a⁻¹
source
@[simp]
theorem equiv.add_left_symm {G : Type u_7} [add_group G] (a : G) :
equiv.symm (equiv.add_left a) = equiv.add_left (-a)
source
@[protected]
def equiv.mul_right {G : Type u_7} [group G] (a : G) :
equiv.perm G

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

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

source
@[simp]
theorem equiv.neg_apply (G : Type u_7) [add_group G] :
⇑(equiv.neg G) = λ (a : G), -a
source
@[protected]
def equiv.neg (G : Type u_7) [add_group G] :
equiv.perm G

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

source
@[simp]
theorem equiv.inv_apply (G : Type u_7) [group G] :
⇑(equiv.inv G) = λ (a : G), a⁻¹
source
@[protected]
def equiv.inv (G : Type u_7) [group G] :
equiv.perm G

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

Equations
source
@[simp]
theorem equiv.neg_symm {G : Type u_7} [add_group G] :
equiv.symm (equiv.neg G) = equiv.neg G
source
@[simp]
theorem equiv.inv_symm {G : Type u_7} [group G] :
equiv.symm (equiv.inv G) = equiv.inv G
source
@[protected]
def equiv.mul_left' {G : Type u_7} [group_with_zero G] (a : G) (ha : a ≠ 0) :
equiv.perm G

Left multiplication by a nonzero element in a group_with_zero is a permutation of the underlying type.

Equations
source
@[simp]
theorem equiv.mul_left'_apply {G : Type u_7} [group_with_zero G] (a : G) (ha : a ≠ 0) :
⇑(equiv.mul_left' a ha) = λ (x : G), a * x
source
@[simp]
theorem equiv.mul_left'_symm_apply {G : Type u_7} [group_with_zero G] (a : G) (ha : a ≠ 0) :
⇑(equiv.symm (equiv.mul_left' a ha)) = λ (x : G), a⁻¹ * x
source
@[protected]
def equiv.mul_right' {G : Type u_7} [group_with_zero G] (a : G) (ha : a ≠ 0) :
equiv.perm G

Right multiplication by a nonzero element in a group_with_zero is a permutation of the underlying type.

Equations
source
@[simp]
theorem equiv.mul_right'_apply {G : Type u_7} [group_with_zero G] (a : G) (ha : a ≠ 0) :
⇑(equiv.mul_right' a ha) = λ (x : G), x * a
source
@[simp]
theorem equiv.mul_right'_symm_apply {G : Type u_7} [group_with_zero G] (a : G) (ha : a ≠ 0) :
⇑(equiv.symm (equiv.mul_right' a ha)) = λ (x : G), x * a⁻¹
source
def add_equiv.neg (G : Type u_1) [add_comm_group G] :
G ≃+ G

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

source
def mul_equiv.inv (G : Type u_1) [comm_group G] :
G ≃* G

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

Equations
source
def add_equiv.to_multiplicative {G : Type u_7} {H : Type u_8} [add_zero_class G] [add_zero_class H] :
G ≃+ H ≃ (multiplicative G ≃* multiplicative H)

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

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

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

Equations
source
def add_equiv.to_multiplicative' {G : Type u_7} {H : Type u_8} [mul_one_class G] [add_zero_class H] :
additive G ≃+ H ≃ (G ≃* multiplicative H)

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

Equations
source
def mul_equiv.to_additive' {G : Type u_7} {H : Type u_8} [mul_one_class G] [add_zero_class H] :
G ≃* multiplicative H ≃ (additive G ≃+ H)

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

Equations
source
def add_equiv.to_multiplicative'' {G : Type u_7} {H : Type u_8} [add_zero_class G] [mul_one_class H] :
G ≃+ additive H ≃ (multiplicative G ≃* H)

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

Equations
source
def mul_equiv.to_additive'' {G : Type u_7} {H : Type u_8} [add_zero_class G] [mul_one_class H] :
multiplicative G ≃* H ≃ (G ≃+ additive H)

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

Equations