# Documentation

Mathlib.Algebra.Group.Equiv.Basic

# Multiplicative and additive equivs #

In this file we define two extensions of Equiv called AddEquiv and MulEquiv, which are datatypes representing isomorphisms of AddMonoids/AddGroups and Monoids/Groups.

## Notations #

• infix  ≃* :25 := MulEquiv
• infix  ≃+ :25 := AddEquiv

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

## Tags #

def ZeroHom.inverse {M : Type u_6} {N : Type u_7} [Zero M] [Zero N] (f : ZeroHom M N) (g : NM) (h₁ : ) :

Make a ZeroHom inverse from the bijective inverse of a ZeroHom

Equations
Instances For
theorem ZeroHom.inverse.proof_1 {M : Type u_1} {N : Type u_2} [Zero M] [Zero N] (f : ZeroHom M N) (g : NM) (h₁ : ) :
g 0 = 0
@[simp]
theorem OneHom.inverse_apply {M : Type u_6} {N : Type u_7} [One M] [One N] (f : OneHom M N) (g : NM) (h₁ : ) :
∀ (a : N), (OneHom.inverse f g h₁) a = g a
@[simp]
theorem ZeroHom.inverse_apply {M : Type u_6} {N : Type u_7} [Zero M] [Zero N] (f : ZeroHom M N) (g : NM) (h₁ : ) :
∀ (a : N), (ZeroHom.inverse f g h₁) a = g a
def OneHom.inverse {M : Type u_6} {N : Type u_7} [One M] [One N] (f : OneHom M N) (g : NM) (h₁ : ) :
OneHom N M

Makes a OneHom inverse from the bijective inverse of a OneHom

Equations
Instances For
theorem AddHom.inverse.proof_1 {M : Type u_1} {N : Type u_2} [Add M] [Add N] (f : AddHom M N) (g : NM) (h₁ : ) (h₂ : ) (x : N) (y : N) :
g (x + y) = g x + g y
def AddHom.inverse {M : Type u_6} {N : Type u_7} [Add M] [Add N] (f : AddHom M N) (g : NM) (h₁ : ) (h₂ : ) :

Equations
• AddHom.inverse f g h₁ h₂ = { toFun := g, map_add' := (_ : ∀ (x y : N), g (x + y) = g x + g y) }
Instances For
@[simp]
theorem AddHom.inverse_apply {M : Type u_6} {N : Type u_7} [Add M] [Add N] (f : AddHom M N) (g : NM) (h₁ : ) (h₂ : ) :
∀ (a : N), (AddHom.inverse f g h₁ h₂) a = g a
@[simp]
theorem MulHom.inverse_apply {M : Type u_6} {N : Type u_7} [Mul M] [Mul N] (f : M →ₙ* N) (g : NM) (h₁ : ) (h₂ : ) :
∀ (a : N), (MulHom.inverse f g h₁ h₂) a = g a
def MulHom.inverse {M : Type u_6} {N : Type u_7} [Mul M] [Mul N] (f : M →ₙ* N) (g : NM) (h₁ : ) (h₂ : ) :

Makes a multiplicative inverse from a bijection which preserves multiplication.

Equations
• MulHom.inverse f g h₁ h₂ = { toFun := g, map_mul' := (_ : ∀ (x y : N), g (x * y) = g x * g y) }
Instances For
def AddMonoidHom.inverse {A : Type u_12} {B : Type u_13} [] [] (f : A →+ B) (g : BA) (h₁ : ) (h₂ : ) :
B →+ A

The inverse of a bijective AddMonoidHom is an AddMonoidHom.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem AddMonoidHom.inverse.proof_2 {A : Type u_1} {B : Type u_2} [] [] (f : A →+ B) (g : BA) (h₁ : ) (h₂ : ) (x : B) (y : B) :
theorem AddMonoidHom.inverse.proof_1 {A : Type u_1} {B : Type u_2} [] [] (f : A →+ B) (g : BA) (h₁ : ) :
ZeroHom.toFun (ZeroHom.inverse (f) g h₁) 0 = 0
@[simp]
theorem MonoidHom.inverse_apply {A : Type u_12} {B : Type u_13} [] [] (f : A →* B) (g : BA) (h₁ : ) (h₂ : ) :
∀ (a : B), (MonoidHom.inverse f g h₁ h₂) a = g a
@[simp]
theorem AddMonoidHom.inverse_apply {A : Type u_12} {B : Type u_13} [] [] (f : A →+ B) (g : BA) (h₁ : ) (h₂ : ) :
∀ (a : B), (AddMonoidHom.inverse f g h₁ h₂) a = g a
def MonoidHom.inverse {A : Type u_12} {B : Type u_13} [] [] (f : A →* B) (g : BA) (h₁ : ) (h₂ : ) :
B →* A

The inverse of a bijective MonoidHom is a MonoidHom.

Equations
• One or more equations did not get rendered due to their size.
Instances For
Type (max u_12 u_13)

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

Instances For
class AddEquivClass (F : Type u_12) (A : outParam (Type u_13)) (B : outParam (Type u_14)) [Add A] [Add B] extends :
Type (max (max u_12 u_13) u_14)

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

• coe : FAB
• inv : FBA
• left_inv : ∀ (e : F),
• right_inv : ∀ (e : F),
• coe_injective' : ∀ (e g : F), e = g
• map_add : ∀ (f : F) (a b : A), f (a + b) = f a + f b

Instances
@[reducible]

The AddHom underlying an AddEquiv.

Equations
Instances For
structure MulEquiv (M : Type u_12) (N : Type u_13) [Mul M] [Mul N] extends :
Type (max u_12 u_13)

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

Instances For
@[reducible]
abbrev MulEquiv.toMulHom {M : Type u_12} {N : Type u_13} [Mul M] [Mul N] (self : M ≃* N) :

The MulHom underlying a MulEquiv.

Equations
Instances For
class MulEquivClass (F : Type u_12) (A : outParam (Type u_13)) (B : outParam (Type u_14)) [Mul A] [Mul B] extends :
Type (max (max u_12 u_13) u_14)

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

• coe : FAB
• inv : FBA
• left_inv : ∀ (e : F),
• right_inv : ∀ (e : F),
• coe_injective' : ∀ (e g : F), e = g
• map_mul : ∀ (f : F) (a b : A), f (a * b) = f a * f b

Preserves multiplication.

Instances

Notation for a MulEquiv.

Equations
Instances For

Notation for an AddEquiv.

Equations
Instances For
Function.Injective FunLike.coe
Equations
instance MulEquivClass.instMulHomClass {M : Type u_6} {N : Type u_7} (F : Type u_12) [Mul M] [Mul N] [h : ] :
Equations
theorem AddEquivClass.instAddMonoidHomClass.proof_3 (F : Type u_3) {M : Type u_2} {N : Type u_1} [] [] [] (e : F) :
e 0 = 0
instance AddEquivClass.instAddMonoidHomClass (F : Type u_1) {M : Type u_6} {N : Type u_7} [] [] [] :
Equations
theorem AddEquivClass.instAddMonoidHomClass.proof_2 (F : Type u_3) {M : Type u_2} {N : Type u_1} [] [] [] (f : F) (x : M) (y : M) :
f (x + y) = f x + f y
theorem AddEquivClass.instAddMonoidHomClass.proof_1 (F : Type u_1) {M : Type u_2} {N : Type u_3} [] [] [] :
Function.Injective FunLike.coe
instance MulEquivClass.instMonoidHomClass (F : Type u_1) {M : Type u_6} {N : Type u_7} [] [] [] :
Equations
instance MulEquivClass.toZeroHomClass (F : Type u_1) {α : Type u_2} {β : Type u_3} [] [] [] :
ZeroHomClass F α β
Equations
instance MulEquivClass.toMonoidWithZeroHomClass (F : Type u_1) {α : Type u_2} {β : Type u_3} [] [] [] :
Equations
@[simp]
theorem AddEquivClass.map_eq_zero_iff {F : Type u_1} {M : Type u_12} {N : Type u_13} [] [] [] (h : F) {x : M} :
h x = 0 x = 0
@[simp]
theorem MulEquivClass.map_eq_one_iff {F : Type u_1} {M : Type u_12} {N : Type u_13} [] [] [] (h : F) {x : M} :
h x = 1 x = 1
theorem AddEquivClass.map_ne_zero_iff {F : Type u_1} {M : Type u_12} {N : Type u_13} [] [] [] (h : F) {x : M} :
h x 0 x 0
theorem MulEquivClass.map_ne_one_iff {F : Type u_1} {M : Type u_12} {N : Type u_13} [] [] [] (h : F) {x : M} :
h x 1 x 1
def AddEquivClass.toAddEquiv {F : Type u_1} {α : Type u_2} {β : Type u_3} [Add α] [Add β] [] (f : F) :
α ≃+ β

Turn an element of a type F satisfying AddEquivClass F α β into an actual AddEquiv. This is declared as the default coercion from F to α ≃+ β.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def MulEquivClass.toMulEquiv {F : Type u_1} {α : Type u_2} {β : Type u_3} [Mul α] [Mul β] [] (f : F) :
α ≃* β

Turn an element of a type F satisfying MulEquivClass F α β into an actual MulEquiv. This is declared as the default coercion from F to α ≃* β.

Equations
• One or more equations did not get rendered due to their size.
Instances For
instance instCoeTCAddEquiv {F : Type u_1} {α : Type u_2} {β : Type u_3} [Add α] [Add β] [] :
CoeTC F (α ≃+ β)

Any type satisfying AddEquivClass can be cast into AddEquiv via AddEquivClass.toAddEquiv.

Equations
instance instCoeTCMulEquiv {F : Type u_1} {α : Type u_2} {β : Type u_3} [Mul α] [Mul β] [] :
CoeTC F (α ≃* β)

Any type satisfying MulEquivClass can be cast into MulEquiv via MulEquivClass.toMulEquiv.

Equations
• instCoeTCMulEquiv = { coe := MulEquivClass.toMulEquiv }
theorem MulEquivClass.toMulEquiv_injective {F : Type u_1} {α : Type u_2} {β : Type u_3} [Mul α] [Mul β] [] :
Function.Injective MulEquivClass.toMulEquiv
Function.LeftInverse f.invFun f.toFun
theorem AddEquiv.instAddEquivClassAddEquiv.proof_3 {M : Type u_2} {N : Type u_1} [Add M] [Add N] (f : M ≃+ N) (g : M ≃+ N) (h₁ : (fun (f : M ≃+ N) => f.toFun) f = (fun (f : M ≃+ N) => f.toFun) g) (h₂ : (fun (f : M ≃+ N) => f.invFun) f = (fun (f : M ≃+ N) => f.invFun) g) :
f = g
Function.RightInverse f.invFun f.toFun
Equations
instance MulEquiv.instMulEquivClassMulEquiv {M : Type u_6} {N : Type u_7} [Mul M] [Mul N] :
Equations
CoeFun (M ≃+ N) fun (x : M ≃+ N) => MN
Equations
• AddEquiv.instCoeFunAddEquivForAll = { coe := fun (f : M ≃+ N) => f }
instance MulEquiv.instCoeFunMulEquivForAll {M : Type u_6} {N : Type u_7} [Mul M] [Mul N] :
CoeFun (M ≃* N) fun (x : M ≃* N) => MN
Equations
• MulEquiv.instCoeFunMulEquivForAll = { coe := fun (f : M ≃* N) => f }
@[simp]
theorem AddEquiv.toEquiv_eq_coe {M : Type u_6} {N : Type u_7} [Add M] [Add N] (f : M ≃+ N) :
f.toEquiv = f
@[simp]
theorem MulEquiv.toEquiv_eq_coe {M : Type u_6} {N : Type u_7} [Mul M] [Mul N] (f : M ≃* N) :
f.toEquiv = f
@[simp]
@[simp]
theorem MulEquiv.toMulHom_eq_coe {M : Type u_6} {N : Type u_7} [Mul M] [Mul N] (f : M ≃* N) :
@[simp]
theorem AddEquiv.coe_toEquiv {M : Type u_6} {N : Type u_7} [Add M] [Add N] (f : M ≃+ N) :
f = f
@[simp]
theorem MulEquiv.coe_toEquiv {M : Type u_6} {N : Type u_7} [Mul M] [Mul N] (f : M ≃* N) :
f = f
@[simp]
= f
@[simp]
theorem MulEquiv.coe_toMulHom {M : Type u_6} {N : Type u_7} [Mul M] [Mul N] {f : M ≃* N} :
= f
theorem AddEquiv.map_add {M : Type u_6} {N : Type u_7} [Add M] [Add N] (f : M ≃+ N) (x : M) (y : M) :
f (x + y) = f x + f y

theorem MulEquiv.map_mul {M : Type u_6} {N : Type u_7} [Mul M] [Mul N] (f : M ≃* N) (x : M) (y : M) :
f (x * y) = f x * f y

A multiplicative isomorphism preserves multiplication.

def AddEquiv.mk' {M : Type u_6} {N : Type u_7} [Add M] [Add N] (f : M N) (h : ∀ (x y : M), f (x + y) = f x + f y) :
M ≃+ N

Equations
• = { toEquiv := f, map_add' := h }
Instances For
def MulEquiv.mk' {M : Type u_6} {N : Type u_7} [Mul M] [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
• = { toEquiv := f, map_mul' := h }
Instances For
theorem AddEquiv.bijective {M : Type u_6} {N : Type u_7} [Add M] [Add N] (e : M ≃+ N) :
theorem MulEquiv.bijective {M : Type u_6} {N : Type u_7} [Mul M] [Mul N] (e : M ≃* N) :
theorem AddEquiv.injective {M : Type u_6} {N : Type u_7} [Add M] [Add N] (e : M ≃+ N) :
theorem MulEquiv.injective {M : Type u_6} {N : Type u_7} [Mul M] [Mul N] (e : M ≃* N) :
theorem AddEquiv.surjective {M : Type u_6} {N : Type u_7} [Add M] [Add N] (e : M ≃+ N) :
theorem MulEquiv.surjective {M : Type u_6} {N : Type u_7} [Mul M] [Mul N] (e : M ≃* N) :
M ≃+ M

The identity map is an additive isomorphism.

Equations
• One or more equations did not get rendered due to their size.
Instances For
∀ (x x_1 : M), Equiv.toFun { toFun := ().toFun, invFun := ().invFun, left_inv := (_ : Function.LeftInverse ().invFun ().toFun), right_inv := (_ : Function.RightInverse ().invFun ().toFun) } (x + x_1) = Equiv.toFun { toFun := ().toFun, invFun := ().invFun, left_inv := (_ : Function.LeftInverse ().invFun ().toFun), right_inv := (_ : Function.RightInverse ().invFun ().toFun) } (x + x_1)
def MulEquiv.refl (M : Type u_12) [Mul M] :
M ≃* M

The identity map is a multiplicative isomorphism.

Equations
• One or more equations did not get rendered due to their size.
Instances For
Equations
instance MulEquiv.instInhabitedMulEquiv {M : Type u_6} [Mul M] :
Equations
• MulEquiv.instInhabitedMulEquiv = { default := }
theorem AddEquiv.symm_map_add {M : Type u_12} {N : Type u_13} [Add M] [Add N] (h : M ≃+ N) (x : N) (y : N) :
h.symm (x + y) = h.symm x + h.symm y
theorem MulEquiv.symm_map_mul {M : Type u_12} {N : Type u_13} [Mul M] [Mul N] (h : M ≃* N) (x : N) (y : N) :
h.symm (x * y) = h.symm x * h.symm y

An alias for h.symm.map_mul. Introduced to fix the issue in https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/!4.234183.20.60simps.60.20maximum.20recursion.20depth

def AddEquiv.symm {M : Type u_12} {N : Type u_13} [Add M] [Add N] (h : M ≃+ N) :
N ≃+ M

The inverse of an isomorphism is an isomorphism.

Equations
• = { toEquiv := h.symm, map_add' := (_ : ∀ (x y : N), h.symm (x + y) = h.symm x + h.symm y) }
Instances For
def MulEquiv.symm {M : Type u_12} {N : Type u_13} [Mul M] [Mul N] (h : M ≃* N) :
N ≃* M

The inverse of an isomorphism is an isomorphism.

Equations
• = { toEquiv := h.symm, map_mul' := (_ : ∀ (x y : N), h.symm (x * y) = h.symm x * h.symm y) }
Instances For
theorem AddEquiv.invFun_eq_symm {M : Type u_6} {N : Type u_7} [Add M] [Add N] {f : M ≃+ N} :
f.invFun = ()
theorem MulEquiv.invFun_eq_symm {M : Type u_6} {N : Type u_7} [Mul M] [Mul N] {f : M ≃* N} :
f.invFun = ()
@[simp]
theorem AddEquiv.coe_toEquiv_symm {M : Type u_6} {N : Type u_7} [Add M] [Add N] (f : M ≃+ N) :
(f).symm = ()
@[simp]
theorem MulEquiv.coe_toEquiv_symm {M : Type u_6} {N : Type u_7} [Mul M] [Mul N] (f : M ≃* N) :
(f).symm = ()
@[simp]
theorem AddEquiv.equivLike_neg_eq_symm {M : Type u_6} {N : Type u_7} [Add M] [Add N] (f : M ≃+ N) :
= ()
@[simp]
theorem MulEquiv.equivLike_inv_eq_symm {M : Type u_6} {N : Type u_7} [Mul M] [Mul N] (f : M ≃* N) :
= ()
def AddEquiv.Simps.symm_apply {M : Type u_6} {N : Type u_7} [Add M] [Add N] (e : M ≃+ N) :
NM

See Note [custom simps projection]

Equations
Instances For
def MulEquiv.Simps.symm_apply {M : Type u_6} {N : Type u_7} [Mul M] [Mul N] (e : M ≃* N) :
NM

See Note [custom simps projection]

Equations
Instances For
@[simp]
theorem AddEquiv.toEquiv_symm {M : Type u_6} {N : Type u_7} [Add M] [Add N] (f : M ≃+ N) :
() = (f).symm
@[simp]
theorem MulEquiv.toEquiv_symm {M : Type u_6} {N : Type u_7} [Mul M] [Mul N] (f : M ≃* N) :
() = (f).symm
@[simp]
theorem AddEquiv.coe_mk {M : Type u_6} {N : Type u_7} [Add M] [Add N] (f : M N) (hf : ∀ (x y : M), f (x + y) = f x + f y) :
{ toEquiv := f, map_add' := hf } = f
@[simp]
theorem MulEquiv.coe_mk {M : Type u_6} {N : Type u_7} [Mul M] [Mul N] (f : M N) (hf : ∀ (x y : M), f (x * y) = f x * f y) :
{ toEquiv := f, map_mul' := hf } = f
@[simp]
theorem AddEquiv.symm_symm {M : Type u_6} {N : Type u_7} [Add M] [Add N] (f : M ≃+ N) :
@[simp]
theorem MulEquiv.symm_symm {M : Type u_6} {N : Type u_7} [Mul M] [Mul N] (f : M ≃* N) :
theorem MulEquiv.symm_bijective {M : Type u_6} {N : Type u_7} [Mul M] [Mul N] :
Function.Bijective MulEquiv.symm
@[simp]
theorem AddEquiv.symm_mk {M : Type u_6} {N : Type u_7} [Add M] [Add N] (f : M N) (h : ∀ (x y : M), Equiv.toFun f (x + y) = + ) :
AddEquiv.symm { toEquiv := f, map_add' := h } = { toEquiv := f.symm, map_add' := (_ : ∀ (x y : N), { toEquiv := f, map_add' := h }.symm (x + y) = { toEquiv := f, map_add' := h }.symm x + { toEquiv := f, map_add' := h }.symm y) }
@[simp]
theorem MulEquiv.symm_mk {M : Type u_6} {N : Type u_7} [Mul M] [Mul N] (f : M N) (h : ∀ (x y : M), Equiv.toFun f (x * y) = * ) :
MulEquiv.symm { toEquiv := f, map_mul' := h } = { toEquiv := f.symm, map_mul' := (_ : ∀ (x y : N), { toEquiv := f, map_mul' := h }.symm (x * y) = { toEquiv := f, map_mul' := h }.symm x * { toEquiv := f, map_mul' := h }.symm y) }
@[simp]
@[simp]
theorem MulEquiv.refl_symm {M : Type u_6} [Mul M] :
theorem AddEquiv.trans.proof_1 {M : Type u_3} {N : Type u_2} {P : Type u_1} [Add M] [Add N] [Add P] (h1 : M ≃+ N) (h2 : N ≃+ P) (x : M) (y : M) :
h2 (h1 (x + y)) = h2 (h1 x) + h2 (h1 y)
def AddEquiv.trans {M : Type u_6} {N : Type u_7} {P : Type u_8} [Add M] [Add N] [Add P] (h1 : M ≃+ N) (h2 : N ≃+ P) :
M ≃+ P

Equations
• One or more equations did not get rendered due to their size.
Instances For
def MulEquiv.trans {M : Type u_6} {N : Type u_7} {P : Type u_8} [Mul M] [Mul N] [Mul P] (h1 : M ≃* N) (h2 : N ≃* P) :
M ≃* P

Transitivity of multiplication-preserving isomorphisms

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem AddEquiv.apply_symm_apply {M : Type u_6} {N : Type u_7} [Add M] [Add N] (e : M ≃+ N) (y : N) :
e (() y) = y

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

@[simp]
theorem MulEquiv.apply_symm_apply {M : Type u_6} {N : Type u_7} [Mul M] [Mul N] (e : M ≃* N) (y : N) :
e (() y) = y

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

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

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

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

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

@[simp]
theorem AddEquiv.symm_comp_self {M : Type u_6} {N : Type u_7} [Add M] [Add N] (e : M ≃+ N) :
() e = id
@[simp]
theorem MulEquiv.symm_comp_self {M : Type u_6} {N : Type u_7} [Mul M] [Mul N] (e : M ≃* N) :
() e = id
@[simp]
theorem AddEquiv.self_comp_symm {M : Type u_6} {N : Type u_7} [Add M] [Add N] (e : M ≃+ N) :
e () = id
@[simp]
theorem MulEquiv.self_comp_symm {M : Type u_6} {N : Type u_7} [Mul M] [Mul N] (e : M ≃* N) :
e () = id
@[simp]
() = id
@[simp]
theorem MulEquiv.coe_refl {M : Type u_6} [Mul M] :
() = id
@[simp]
theorem AddEquiv.refl_apply {M : Type u_6} [Add M] (m : M) :
() m = m
@[simp]
theorem MulEquiv.refl_apply {M : Type u_6} [Mul M] (m : M) :
() m = m
@[simp]
theorem AddEquiv.coe_trans {M : Type u_6} {N : Type u_7} {P : Type u_8} [Add M] [Add N] [Add P] (e₁ : M ≃+ N) (e₂ : N ≃+ P) :
(AddEquiv.trans e₁ e₂) = e₂ e₁
@[simp]
theorem MulEquiv.coe_trans {M : Type u_6} {N : Type u_7} {P : Type u_8} [Mul M] [Mul N] [Mul P] (e₁ : M ≃* N) (e₂ : N ≃* P) :
(MulEquiv.trans e₁ e₂) = e₂ e₁
@[simp]
theorem AddEquiv.trans_apply {M : Type u_6} {N : Type u_7} {P : Type u_8} [Add M] [Add N] [Add P] (e₁ : M ≃+ N) (e₂ : N ≃+ P) (m : M) :
(AddEquiv.trans e₁ e₂) m = e₂ (e₁ m)
@[simp]
theorem MulEquiv.trans_apply {M : Type u_6} {N : Type u_7} {P : Type u_8} [Mul M] [Mul N] [Mul P] (e₁ : M ≃* N) (e₂ : N ≃* P) (m : M) :
(MulEquiv.trans e₁ e₂) m = e₂ (e₁ m)
@[simp]
theorem AddEquiv.symm_trans_apply {M : Type u_6} {N : Type u_7} {P : Type u_8} [Add M] [Add N] [Add P] (e₁ : M ≃+ N) (e₂ : N ≃+ P) (p : P) :
@[simp]
theorem MulEquiv.symm_trans_apply {M : Type u_6} {N : Type u_7} {P : Type u_8} [Mul M] [Mul N] [Mul P] (e₁ : M ≃* N) (e₂ : N ≃* P) (p : P) :
(MulEquiv.symm (MulEquiv.trans e₁ e₂)) p = () (() p)
theorem AddEquiv.apply_eq_iff_eq {M : Type u_6} {N : Type u_7} [Add M] [Add N] (e : M ≃+ N) {x : M} {y : M} :
e x = e y x = y
theorem MulEquiv.apply_eq_iff_eq {M : Type u_6} {N : Type u_7} [Mul M] [Mul N] (e : M ≃* N) {x : M} {y : M} :
e x = e y x = y
theorem AddEquiv.apply_eq_iff_symm_apply {M : Type u_6} {N : Type u_7} [Add M] [Add N] (e : M ≃+ N) {x : M} {y : N} :
e x = y x = () y
theorem MulEquiv.apply_eq_iff_symm_apply {M : Type u_6} {N : Type u_7} [Mul M] [Mul N] (e : M ≃* N) {x : M} {y : N} :
e x = y x = () y
theorem AddEquiv.symm_apply_eq {M : Type u_6} {N : Type u_7} [Add M] [Add N] (e : M ≃+ N) {x : N} {y : M} :
() x = y x = e y
theorem MulEquiv.symm_apply_eq {M : Type u_6} {N : Type u_7} [Mul M] [Mul N] (e : M ≃* N) {x : N} {y : M} :
() x = y x = e y
theorem AddEquiv.eq_symm_apply {M : Type u_6} {N : Type u_7} [Add M] [Add N] (e : M ≃+ N) {x : N} {y : M} :
y = () x e y = x
theorem MulEquiv.eq_symm_apply {M : Type u_6} {N : Type u_7} [Mul M] [Mul N] (e : M ≃* N) {x : N} {y : M} :
y = () x e y = x
theorem AddEquiv.eq_comp_symm {M : Type u_6} {N : Type u_7} [Add M] [Add N] {α : Type u_12} (e : M ≃+ N) (f : Nα) (g : Mα) :
f = g () f e = g
theorem MulEquiv.eq_comp_symm {M : Type u_6} {N : Type u_7} [Mul M] [Mul N] {α : Type u_12} (e : M ≃* N) (f : Nα) (g : Mα) :
f = g () f e = g
theorem AddEquiv.comp_symm_eq {M : Type u_6} {N : Type u_7} [Add M] [Add N] {α : Type u_12} (e : M ≃+ N) (f : Nα) (g : Mα) :
g () = f g = f e
theorem MulEquiv.comp_symm_eq {M : Type u_6} {N : Type u_7} [Mul M] [Mul N] {α : Type u_12} (e : M ≃* N) (f : Nα) (g : Mα) :
g () = f g = f e
theorem AddEquiv.eq_symm_comp {M : Type u_6} {N : Type u_7} [Add M] [Add N] {α : Type u_12} (e : M ≃+ N) (f : αM) (g : αN) :
f = () g e f = g
theorem MulEquiv.eq_symm_comp {M : Type u_6} {N : Type u_7} [Mul M] [Mul N] {α : Type u_12} (e : M ≃* N) (f : αM) (g : αN) :
f = () g e f = g
theorem AddEquiv.symm_comp_eq {M : Type u_6} {N : Type u_7} [Add M] [Add N] {α : Type u_12} (e : M ≃+ N) (f : αM) (g : αN) :
() g = f g = e f
theorem MulEquiv.symm_comp_eq {M : Type u_6} {N : Type u_7} [Mul M] [Mul N] {α : Type u_12} (e : M ≃* N) (f : αM) (g : αN) :
() g = f g = e f
@[simp]
theorem AddEquiv.symm_trans_self {M : Type u_6} {N : Type u_7} [Add M] [Add N] (e : M ≃+ N) :
@[simp]
theorem MulEquiv.symm_trans_self {M : Type u_6} {N : Type u_7} [Mul M] [Mul N] (e : M ≃* N) :
@[simp]
theorem AddEquiv.self_trans_symm {M : Type u_6} {N : Type u_7} [Add M] [Add N] (e : M ≃+ N) :
@[simp]
theorem MulEquiv.self_trans_symm {M : Type u_6} {N : Type u_7} [Mul M] [Mul N] (e : M ≃* N) :
theorem MulEquiv.coe_monoidHom_refl {M : Type u_12} [] :
() =
theorem AddEquiv.coe_addMonoidHom_trans {M : Type u_12} {N : Type u_13} {P : Type u_14} [] [] [] (e₁ : M ≃+ N) (e₂ : N ≃+ P) :
theorem MulEquiv.coe_monoidHom_trans {M : Type u_12} {N : Type u_13} {P : Type u_14} [] [] [] (e₁ : M ≃* N) (e₂ : N ≃* P) :
(MulEquiv.trans e₁ e₂) = MonoidHom.comp e₂ e₁
theorem AddEquiv.ext {M : Type u_6} {N : Type u_7} [Add M] [Add N] {f : M ≃+ N} {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.

theorem MulEquiv.ext {M : Type u_6} {N : Type u_7} [Mul M] [Mul N] {f : M ≃* N} {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 AddEquiv.ext_iff {M : Type u_6} {N : Type u_7} [Add M] [Add N] {f : M ≃+ N} {g : M ≃+ N} :
f = g ∀ (x : M), f x = g x
theorem MulEquiv.ext_iff {M : Type u_6} {N : Type u_7} [Mul M] [Mul N] {f : M ≃* N} {g : M ≃* N} :
f = g ∀ (x : M), f x = g x
@[simp]
theorem AddEquiv.mk_coe {M : Type u_6} {N : Type u_7} [Add M] [Add N] (e : M ≃+ N) (e' : NM) (h₁ : ) (h₂ : ) (h₃ : ∀ (x y : M), Equiv.toFun { toFun := e, invFun := e', left_inv := h₁, right_inv := h₂ } (x + y) = Equiv.toFun { toFun := e, invFun := e', left_inv := h₁, right_inv := h₂ } x + Equiv.toFun { toFun := e, invFun := e', left_inv := h₁, right_inv := h₂ } y) :
{ toEquiv := { toFun := e, invFun := e', left_inv := h₁, right_inv := h₂ }, map_add' := h₃ } = e
@[simp]
theorem MulEquiv.mk_coe {M : Type u_6} {N : Type u_7} [Mul M] [Mul N] (e : M ≃* N) (e' : NM) (h₁ : ) (h₂ : ) (h₃ : ∀ (x y : M), Equiv.toFun { toFun := e, invFun := e', left_inv := h₁, right_inv := h₂ } (x * y) = Equiv.toFun { toFun := e, invFun := e', left_inv := h₁, right_inv := h₂ } x * Equiv.toFun { toFun := e, invFun := e', left_inv := h₁, right_inv := h₂ } y) :
{ toEquiv := { toFun := e, invFun := e', left_inv := h₁, right_inv := h₂ }, map_mul' := h₃ } = e
@[simp]
theorem AddEquiv.mk_coe' {M : Type u_6} {N : Type u_7} [Add M] [Add N] (e : M ≃+ N) (f : NM) (h₁ : Function.LeftInverse (e) f) (h₂ : ) (h₃ : ∀ (x y : N), Equiv.toFun { toFun := f, invFun := e, left_inv := h₁, right_inv := h₂ } (x + y) = Equiv.toFun { toFun := f, invFun := e, left_inv := h₁, right_inv := h₂ } x + Equiv.toFun { toFun := f, invFun := e, left_inv := h₁, right_inv := h₂ } y) :
{ toEquiv := { toFun := f, invFun := e, left_inv := h₁, right_inv := h₂ }, map_add' := h₃ } =
@[simp]
theorem MulEquiv.mk_coe' {M : Type u_6} {N : Type u_7} [Mul M] [Mul N] (e : M ≃* N) (f : NM) (h₁ : Function.LeftInverse (e) f) (h₂ : ) (h₃ : ∀ (x y : N), Equiv.toFun { toFun := f, invFun := e, left_inv := h₁, right_inv := h₂ } (x * y) = Equiv.toFun { toFun := f, invFun := e, left_inv := h₁, right_inv := h₂ } x * Equiv.toFun { toFun := f, invFun := e, left_inv := h₁, right_inv := h₂ } y) :
{ toEquiv := { toFun := f, invFun := e, left_inv := h₁, right_inv := h₂ }, map_mul' := h₃ } =
theorem AddEquiv.congr_arg {M : Type u_6} {N : Type u_7} [Add M] [Add N] {f : M ≃+ N} {x : M} {x' : M} :
x = x'f x = f x'
theorem MulEquiv.congr_arg {M : Type u_6} {N : Type u_7} [Mul M] [Mul N] {f : M ≃* N} {x : M} {x' : M} :
x = x'f x = f x'
theorem AddEquiv.congr_fun {M : Type u_6} {N : Type u_7} [Add M] [Add N] {f : M ≃+ N} {g : M ≃+ N} (h : f = g) (x : M) :
f x = g x
theorem MulEquiv.congr_fun {M : Type u_6} {N : Type u_7} [Mul M] [Mul N] {f : M ≃* N} {g : M ≃* N} (h : f = g) (x : M) :
f x = g x
∀ (x x_1 : M), Equiv.toFun { toFun := ().toFun, invFun := ().invFun, left_inv := (_ : Function.LeftInverse ().invFun ().toFun), right_inv := (_ : Function.RightInverse ().invFun ().toFun) } (x + x_1) = Equiv.toFun { toFun := ().toFun, invFun := ().invFun, left_inv := (_ : Function.LeftInverse ().invFun ().toFun), right_inv := (_ : Function.RightInverse ().invFun ().toFun) } x + Equiv.toFun { toFun := ().toFun, invFun := ().invFun, left_inv := (_ : Function.LeftInverse ().invFun ().toFun), right_inv := (_ : Function.RightInverse ().invFun ().toFun) } x_1
M ≃+ N

The AddEquiv between two AddMonoids with a unique element.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def MulEquiv.mulEquivOfUnique {M : Type u_12} {N : Type u_13} [] [] [Mul M] [Mul N] :
M ≃* N

The MulEquiv between two monoids with a unique element.

Equations
• One or more equations did not get rendered due to their size.
Instances For
Unique (M ≃+ N)

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

Equations
• AddEquiv.instUniqueAddEquiv = { toInhabited := { default := AddEquiv.addEquivOfUnique }, uniq := (_ : ∀ (x : M ≃+ N), x = default) }
∀ (x : M ≃+ N), x = default
instance MulEquiv.instUniqueMulEquiv {M : Type u_12} {N : Type u_13} [] [] [Mul M] [Mul N] :
Unique (M ≃* N)

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

Equations
• MulEquiv.instUniqueMulEquiv = { toInhabited := { default := MulEquiv.mulEquivOfUnique }, uniq := (_ : ∀ (x : M ≃* N), x = default) }

## Monoids #

theorem AddEquiv.map_zero {M : Type u_12} {N : Type u_13} [] [] (h : M ≃+ N) :
h 0 = 0

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

theorem MulEquiv.map_one {M : Type u_12} {N : Type u_13} [] [] (h : M ≃* N) :
h 1 = 1

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

theorem AddEquiv.map_eq_zero_iff {M : Type u_12} {N : Type u_13} [] [] (h : M ≃+ N) {x : M} :
h x = 0 x = 0
theorem MulEquiv.map_eq_one_iff {M : Type u_12} {N : Type u_13} [] [] (h : M ≃* N) {x : M} :
h x = 1 x = 1
theorem AddEquiv.map_ne_zero_iff {M : Type u_12} {N : Type u_13} [] [] (h : M ≃+ N) {x : M} :
h x 0 x 0
theorem MulEquiv.map_ne_one_iff {M : Type u_12} {N : Type u_13} [] [] (h : M ≃* N) {x : M} :
h x 1 x 1
noncomputable def AddEquiv.ofBijective {M : Type u_12} {N : Type u_13} {F : Type u_14} [Add M] [Add N] [AddHomClass F M N] (f : F) (hf : ) :
M ≃+ N

A bijective AddSemigroup homomorphism is an isomorphism

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem MulEquiv.ofBijective_apply {M : Type u_12} {N : Type u_13} {F : Type u_14} [Mul M] [Mul N] [MulHomClass F M N] (f : F) (hf : ) (a : M) :
() a = f a
@[simp]
theorem AddEquiv.ofBijective_apply {M : Type u_12} {N : Type u_13} {F : Type u_14} [Add M] [Add N] [AddHomClass F M N] (f : F) (hf : ) (a : M) :
() a = f a
noncomputable def MulEquiv.ofBijective {M : Type u_12} {N : Type u_13} {F : Type u_14} [Mul M] [Mul N] [MulHomClass F M N] (f : F) (hf : ) :
M ≃* N

A bijective Semigroup homomorphism is an isomorphism

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem AddEquiv.ofBijective_apply_symm_apply {M : Type u_12} {N : Type u_13} [] [] {n : N} (f : M →+ N) (hf : ) :
f ((Equiv.ofBijective (f) hf).symm n) = n
@[simp]
theorem MulEquiv.ofBijective_apply_symm_apply {M : Type u_12} {N : Type u_13} [] [] {n : N} (f : M →* N) (hf : ) :
f ((Equiv.ofBijective (f) hf).symm n) = n
def AddEquiv.toAddMonoidHom {M : Type u_12} {N : Type u_13} [] [] (h : M ≃+ N) :
M →+ N

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem AddEquiv.toAddMonoidHom.proof_1 {M : Type u_2} {N : Type u_1} [] [] (h : M ≃+ N) (x : M) (y : M) :
Equiv.toFun h.toEquiv (x + y) = Equiv.toFun h.toEquiv x + Equiv.toFun h.toEquiv y
def MulEquiv.toMonoidHom {M : Type u_12} {N : Type u_13} [] [] (h : M ≃* N) :
M →* N

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem AddEquiv.coe_toAddMonoidHom {M : Type u_12} {N : Type u_13} [] [] (e : M ≃+ N) :
= e
@[simp]
theorem MulEquiv.coe_toMonoidHom {M : Type u_12} {N : Type u_13} [] [] (e : M ≃* N) :
= e
theorem AddEquiv.toAddMonoidHom_injective {M : Type u_12} {N : Type u_13} [] [] :
theorem MulEquiv.toMonoidHom_injective {M : Type u_12} {N : Type u_13} [] [] :
Function.Injective MulEquiv.toMonoidHom
theorem AddEquiv.arrowCongr.proof_2 {M : Type u_4} {N : Type u_1} {P : Type u_3} {Q : Type u_2} [Add P] [Add Q] (f : M N) (g : P ≃+ Q) (k : NQ) :
(fun (h : MP) (n : N) => g (h (f.symm n))) ((fun (k : NQ) (m : M) => () (k (f m))) k) = k
def AddEquiv.arrowCongr {M : Type u_12} {N : Type u_13} {P : Type u_14} {Q : Type u_15} [Add P] [Add Q] (f : M N) (g : P ≃+ Q) :
(MP) ≃+ (NQ)

An additive analogue of Equiv.arrowCongr, where the equivalence between the targets is additive.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem AddEquiv.arrowCongr.proof_1 {M : Type u_1} {N : Type u_4} {P : Type u_2} {Q : Type u_3} [Add P] [Add Q] (f : M N) (g : P ≃+ Q) (h : MP) :
(fun (k : NQ) (m : M) => () (k (f m))) ((fun (h : MP) (n : N) => g (h (f.symm n))) h) = h
theorem AddEquiv.arrowCongr.proof_3 {M : Type u_3} {N : Type u_1} {P : Type u_4} {Q : Type u_2} [Add P] [Add Q] (f : M N) (g : P ≃+ Q) (h : MP) (k : MP) :
Equiv.toFun { toFun := fun (h : MP) (n : N) => g (h (f.symm n)), invFun := fun (k : NQ) (m : M) => () (k (f m)), left_inv := (_ : ∀ (h : MP), (fun (k : NQ) (m : M) => () (k (f m))) ((fun (h : MP) (n : N) => g (h (f.symm n))) h) = h), right_inv := (_ : ∀ (k : NQ), (fun (h : MP) (n : N) => g (h (f.symm n))) ((fun (k : NQ) (m : M) => () (k (f m))) k) = k) } (h + k) = Equiv.toFun { toFun := fun (h : MP) (n : N) => g (h (f.symm n)), invFun := fun (k : NQ) (m : M) => () (k (f m)), left_inv := (_ : ∀ (h : MP), (fun (k : NQ) (m : M) => () (k (f m))) ((fun (h : MP) (n : N) => g (h (f.symm n))) h) = h), right_inv := (_ : ∀ (k : NQ), (fun (h : MP) (n : N) => g (h (f.symm n))) ((fun (k : NQ) (m : M) => () (k (f m))) k) = k) } h + Equiv.toFun { toFun := fun (h : MP) (n : N) => g (h (f.symm n)), invFun := fun (k : NQ) (m : M) => () (k (f m)), left_inv := (_ : ∀ (h : MP), (fun (k : NQ) (m : M) => () (k (f m))) ((fun (h : MP) (n : N) => g (h (f.symm n))) h) = h), right_inv := (_ : ∀ (k : NQ), (fun (h : MP) (n : N) => g (h (f.symm n))) ((fun (k : NQ) (m : M) => () (k (f m))) k) = k) } k
@[simp]
theorem AddEquiv.arrowCongr_apply {M : Type u_12} {N : Type u_13} {P : Type u_14} {Q : Type u_15} [Add P] [Add Q] (f : M N) (g : P ≃+ Q) (h : MP) (n : N) :
() h n = g (h (f.symm n))
@[simp]
theorem MulEquiv.arrowCongr_apply {M : Type u_12} {N : Type u_13} {P : Type u_14} {Q : Type u_15} [Mul P] [Mul Q] (f : M N) (g : P ≃* Q) (h : MP) (n : N) :
() h n = g (h (f.symm n))
def MulEquiv.arrowCongr {M : Type u_12} {N : Type u_13} {P : Type u_14} {Q : Type u_15} [Mul P] [Mul Q] (f : M N) (g : P ≃* Q) :
(MP) ≃* (NQ)

A multiplicative analogue of Equiv.arrowCongr, where the equivalence between the targets is multiplicative.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def AddEquiv.addMonoidHomCongr {M : Type u_12} {N : Type u_13} {P : Type u_14} {Q : Type u_15} [] [] [] [] (f : M ≃+ N) (g : P ≃+ Q) :
(M →+ P) ≃+ (N →+ Q)

An additive analogue of Equiv.arrowCongr, for additive maps from an additive monoid to a commutative additive monoid.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem AddEquiv.addMonoidHomCongr.proof_2 {M : Type u_4} {N : Type u_2} {P : Type u_3} {Q : Type u_1} [] [] [] [] (f : M ≃+ N) (g : P ≃+ Q) (k : N →+ Q) :
(fun (h : M →+ P) => ) ((fun (k : N →+ Q) => ) k) = k
theorem AddEquiv.addMonoidHomCongr.proof_3 {M : Type u_2} {N : Type u_3} {P : Type u_1} {Q : Type u_4} [] [] [] [] (f : M ≃+ N) (g : P ≃+ Q) (h : M →+ P) (k : M →+ P) :
Equiv.toFun { toFun := fun (h : M →+ P) => , invFun := fun (k : N →+ Q) => , left_inv := (_ : ∀ (h : M →+ P), (fun (k : N →+ Q) => ) ((fun (h : M →+ P) => ) h) = h), right_inv := (_ : ∀ (k : N →+ Q), (fun (h : M →+ P) => ) ((fun (k : N →+ Q) => ) k) = k) } (h + k) = Equiv.toFun { toFun := fun (h : M →+ P) => , invFun := fun (k : N →+ Q) => , left_inv := (_ : ∀ (h : M →+ P), (fun (k : N →+ Q) => ) ((fun (h : M →+ P) => ) h) = h), right_inv := (_ : ∀ (k : N →+ Q), (fun (h : M →+ P) => ) ((fun (k : N →+ Q) => ) k) = k) } h + Equiv.toFun { toFun := fun (h : M →+ P) => , invFun := fun (k : N →+ Q) => , left_inv := (_ : ∀ (h : M →+ P), (fun (k : N →+ Q) => ) ((fun (h : M →+ P) => ) h) = h), right_inv := (_ : ∀ (k : N →+ Q), (fun (h : M →+ P) => ) ((fun (k : N →+ Q) => ) k) = k) } k
theorem AddEquiv.addMonoidHomCongr.proof_1 {M : Type u_2} {N : Type u_4} {P : Type u_1} {Q : Type u_3} [] [] [] [] (f : M ≃+ N) (g : P ≃+ Q) (h : M →+ P) :
(fun (k : N →+ Q) => ) ((fun (h : M →+ P) => ) h) = h
@[simp]
theorem MulEquiv.monoidHomCongr_apply {M : Type u_12} {N : Type u_13} {P : Type u_14} {Q : Type u_15} [] [] [] [] (f : M ≃* N) (g : P ≃* Q) (h : M →* P) :
@[simp]
theorem AddEquiv.addMonoidHomCongr_apply {M : Type u_12} {N : Type u_13} {P : Type u_14} {Q : Type u_15} [] [] [] [] (f : M ≃+ N) (g : P ≃+ Q) (h : M →+ P) :
def MulEquiv.monoidHomCongr {M : Type u_12} {N : Type u_13} {P : Type u_14} {Q : Type u_15} [] [] [] [] (f : M ≃* N) (g : P ≃* Q) :
(M →* P) ≃* (N →* Q)

A multiplicative analogue of Equiv.arrowCongr, for multiplicative maps from a monoid to a commutative monoid.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem AddEquiv.piCongrRight.proof_1 {η : Type u_1} {Ms : ηType u_2} {Ns : ηType u_3} [(j : η) → Add (Ms j)] [(j : η) → Add (Ns j)] (es : (j : η) → Ms j ≃+ Ns j) :
Function.LeftInverse (Equiv.piCongrRight fun (j : η) => (es j).toEquiv).invFun (Equiv.piCongrRight fun (j : η) => (es j).toEquiv).toFun
def AddEquiv.piCongrRight {η : Type u_12} {Ms : ηType u_13} {Ns : ηType u_14} [(j : η) → Add (Ms j)] [(j : η) → 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 AddEquiv version of Equiv.piCongrRight, and the dependent version of AddEquiv.arrowCongr.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem AddEquiv.piCongrRight.proof_2 {η : Type u_1} {Ms : ηType u_2} {Ns : ηType u_3} [(j : η) → Add (Ms j)] [(j : η) → Add (Ns j)] (es : (j : η) → Ms j ≃+ Ns j) :
Function.RightInverse (Equiv.piCongrRight fun (j : η) => (es j).toEquiv).invFun (Equiv.piCongrRight fun (j : η) => (es j).toEquiv).toFun
theorem AddEquiv.piCongrRight.proof_3 {η : Type u_1} {Ms : ηType u_3} {Ns : ηType u_2} [(j : η) → Add (Ms j)] [(j : η) → Add (Ns j)] (es : (j : η) → Ms j ≃+ Ns j) (x : (j : η) → Ms j) (y : (j : η) → Ms j) :
Equiv.toFun { toFun := fun (x : (j : η) → Ms j) (j : η) => (es j) (x j), invFun := fun (x : (j : η) → Ns j) (j : η) => (AddEquiv.symm (es j)) (x j), left_inv := (_ : Function.LeftInverse (Equiv.piCongrRight fun (j : η) => (es j).toEquiv).invFun (Equiv.piCongrRight fun (j : η) => (es j).toEquiv).toFun), right_inv := (_ : Function.RightInverse (Equiv.piCongrRight fun (j : η) => (es j).toEquiv).invFun (Equiv.piCongrRight fun (j : η) => (es j).toEquiv).toFun) } (x + y) = Equiv.toFun { toFun := fun (x : (j : η) → Ms j) (j : η) => (es j) (x j), invFun := fun (x : (j : η) → Ns j) (j : η) => (AddEquiv.symm (es j)) (x j), left_inv := (_ : Function.LeftInverse (Equiv.piCongrRight fun (j : η) => (es j).toEquiv).invFun (Equiv.piCongrRight fun (j : η) => (es j).toEquiv).toFun), right_inv := (_ : Function.RightInverse (Equiv.piCongrRight fun (j : η) => (es j).toEquiv).invFun (Equiv.piCongrRight fun (j : η) => (es j).toEquiv).toFun) } x + Equiv.toFun { toFun := fun (x : (j : η) → Ms j) (j : η) => (es j) (x j), invFun := fun (x : (j : η) → Ns j) (j : η) => (AddEquiv.symm (es j)) (x j), left_inv := (_ : Function.LeftInverse (Equiv.piCongrRight fun (j : η) => (es j).toEquiv).invFun (Equiv.piCongrRight fun (j : η) => (es j).toEquiv).toFun), right_inv := (_ : Function.RightInverse (Equiv.piCongrRight fun (j : η) => (es j).toEquiv).invFun (Equiv.piCongrRight fun (j : η) => (es j).toEquiv).toFun) } y
@[simp]
theorem AddEquiv.piCongrRight_apply {η : Type u_12} {Ms : ηType u_13} {Ns : ηType u_14} [(j : η) → Add (Ms j)] [(j : η) → Add (Ns j)] (es : (j : η) → Ms j ≃+ Ns j) (x : (j : η) → Ms j) (j : η) :
x j = (es j) (x j)
@[simp]
theorem MulEquiv.piCongrRight_apply {η : Type u_12} {Ms : ηType u_13} {Ns : ηType u_14} [(j : η) → Mul (Ms j)] [(j : η) → Mul (Ns j)] (es : (j : η) → Ms j ≃* Ns j) (x : (j : η) → Ms j) (j : η) :
x j = (es j) (x j)
def MulEquiv.piCongrRight {η : Type u_12} {Ms : ηType u_13} {Ns : ηType u_14} [(j : η) → Mul (Ms j)] [(j : η) → 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 MulEquiv version of Equiv.piCongrRight, and the dependent version of MulEquiv.arrowCongr.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem AddEquiv.piCongrRight_refl {η : Type u_12} {Ms : ηType u_13} [(j : η) → Add (Ms j)] :
(AddEquiv.piCongrRight fun (j : η) => AddEquiv.refl (Ms j)) = AddEquiv.refl ((j : η) → Ms j)
@[simp]
theorem MulEquiv.piCongrRight_refl {η : Type u_12} {Ms : ηType u_13} [(j : η) → Mul (Ms j)] :
(MulEquiv.piCongrRight fun (j : η) => MulEquiv.refl (Ms j)) = MulEquiv.refl ((j : η) → Ms j)
@[simp]
theorem AddEquiv.piCongrRight_symm {η : Type u_12} {Ms : ηType u_13} {Ns : ηType u_14} [(j : η) → Add (Ms j)] [(j : η) → Add (Ns j)] (es : (j : η) → Ms j ≃+ Ns j) :
@[simp]
theorem MulEquiv.piCongrRight_symm {η : Type u_12} {Ms : ηType u_13} {Ns : ηType u_14} [(j : η) → Mul (Ms j)] [(j : η) → Mul (Ns j)] (es : (j : η) → Ms j ≃* Ns j) :
= MulEquiv.piCongrRight fun (i : η) => MulEquiv.symm (es i)
@[simp]
theorem AddEquiv.piCongrRight_trans {η : Type u_12} {Ms : ηType u_13} {Ns : ηType u_14} {Ps : ηType u_15} [(j : η) → Add (Ms j)] [(j : η) → Add (Ns j)] [(j : η) → Add (Ps j)] (es : (j : η) → Ms j ≃+ Ns j) (fs : (j : η) → Ns j ≃+ Ps j) :
= AddEquiv.piCongrRight fun (i : η) => AddEquiv.trans (es i) (fs i)
@[simp]
theorem MulEquiv.piCongrRight_trans {η : Type u_12} {Ms : ηType u_13} {Ns : ηType u_14} {Ps : ηType u_15} [(j : η) → Mul (Ms j)] [(j : η) → Mul (Ns j)] [(j : η) → Mul (Ps j)] (es : (j : η) → Ms j ≃* Ns j) (fs : (j : η) → Ns j ≃* Ps j) :
= MulEquiv.piCongrRight fun (i : η) => MulEquiv.trans (es i) (fs i)
theorem AddEquiv.piUnique.proof_2 {ι : Type u_1} (M : ιType u_2) [] :
Function.RightInverse ().invFun ().toFun
def AddEquiv.piUnique {ι : Type u_12} (M : ιType u_13) [(j : ι) → Add (M j)] [] :
((j : ι) → M j) ≃+ M default

A family indexed by a type with a unique element is AddEquiv to the element at the single index.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem AddEquiv.piUnique.proof_1 {ι : Type u_1} (M : ιType u_2) [] :
Function.LeftInverse ().invFun ().toFun
theorem AddEquiv.piUnique.proof_3 {ι : Type u_2} (M : ιType u_1) [(j : ι) → Add (M j)] [] :
∀ (x x_1 : (j : ι) → M j), (x + x_1) default = x default + x_1 default
@[simp]
theorem AddEquiv.piUnique_apply {ι : Type u_12} (M : ιType u_13) [(j : ι) → Add (M j)] [] (f : (i : ι) → M i) :
f = f default
@[simp]
theorem MulEquiv.piUnique_apply {ι : Type u_12} (M : ιType u_13) [(j : ι) → Mul (M j)] [] (f : (i : ι) → M i) :
f = f default
@[simp]
theorem MulEquiv.piUnique_symm_apply {ι : Type u_12} (M : ιType u_13) [(j : ι) → Mul (M j)] [] (x : M default) (i : ι) :
x i =
@[simp]
theorem AddEquiv.piUnique_symm_apply {ι : Type u_12} (M : ιType u_13) [(j : ι) → Add (M j)] [] (x : M default) (i : ι) :
x i =
def MulEquiv.piUnique {ι : Type u_12} (M : ιType u_13) [(j : ι) → Mul (M j)] [] :
((j : ι) → M j) ≃* M default

A family indexed by a type with a unique element is MulEquiv to the element at the single index.

Equations
• One or more equations did not get rendered due to their size.
Instances For

# Groups #

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

theorem MulEquiv.map_inv {G : Type u_10} {H : Type u_11} [] [] (h : G ≃* H) (x : G) :
h x⁻¹ = (h x)⁻¹

A multiplicative equivalence of groups preserves inversion.

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

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

A multiplicative equivalence of groups preserves division.

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 toFun = f and invFun = g. This constructor is useful if the underlying type(s) have specialized ext lemmas for additive homomorphisms.

Equations
• One or more equations did not get rendered due to their size.
Instances For
() x = () x
() x = () x
def MulHom.toMulEquiv {M : Type u_6} {N : Type u_7} [Mul M] [Mul N] (f : M →ₙ* N) (g : N →ₙ* M) (h₁ : = ) (h₂ : = ) :
M ≃* N

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
@[simp]
theorem MulHom.toMulEquiv_apply {M : Type u_6} {N : Type u_7} [Mul M] [Mul N] (f : M →ₙ* N) (g : N →ₙ* M) (h₁ : = ) (h₂ : = ) :
(MulHom.toMulEquiv f g h₁ h₂) = f
@[simp]
@[simp]
theorem MulHom.toMulEquiv_symm_apply {M : Type u_6} {N : Type u_7} [Mul M] [Mul N] (f : M →ₙ* N) (g : N →ₙ* M) (h₁ : = ) (h₂ : = ) :
(MulEquiv.symm (MulHom.toMulEquiv f g h₁ h₂)) = g
theorem AddMonoidHom.toAddEquiv.proof_2 {M : Type u_2} {N : Type u_1} [] [] (f : M →+ N) (g : N →+ M) (h₂ : ) (x : N) :
() x = () x
def AddMonoidHom.toAddEquiv {M : Type u_6} {N : Type u_7} [] [] (f : M →+ N) (g : N →+ M) (h₁ : ) (h₂ : ) :
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 toFun = f and invFun = g. This constructor is useful if the underlying type(s) have specialized ext lemmas for additive monoid homomorphisms.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem AddMonoidHom.toAddEquiv.proof_1 {M : Type u_1} {N : Type u_2} [] [] (f : M →+ N) (g : N →+ M) (h₁ : ) (x : M) :
() x = () x
@[simp]
theorem MonoidHom.toMulEquiv_apply {M : Type u_6} {N : Type u_7} [] [] (f : M →* N) (g : N →* M) (h₁ : ) (h₂ : ) :
(MonoidHom.toMulEquiv f g h₁ h₂) = f
@[simp]
theorem AddMonoidHom.toAddEquiv_apply {M : Type u_6} {N : Type u_7} [] [] (f : M →+ N) (g : N →+ M) (h₁ : ) (h₂ : ) :
@[simp]
theorem AddMonoidHom.toAddEquiv_symm_apply {M : Type u_6} {N : Type u_7} [] [] (f : M →+ N) (g : N →+ M) (h₁ : ) (h₂ : ) :
@[simp]
theorem MonoidHom.toMulEquiv_symm_apply {M : Type u_6} {N : Type u_7} [] [] (f : M →* N) (g : N →* M) (h₁ : ) (h₂ : ) :
(MulEquiv.symm (MonoidHom.toMulEquiv f g h₁ h₂)) = g
def MonoidHom.toMulEquiv {M : Type u_6} {N : Type u_7} [] [] (f : M →* N) (g : N →* M) (h₁ : ) (h₂ : ) :
M ≃* N

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
def Equiv.neg (G : Type u_10) [] :

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

Equations
Instances For
@[simp]
theorem Equiv.neg_apply (G : Type u_10) [] :
() = Neg.neg
@[simp]
theorem Equiv.inv_apply (G : Type u_10) [] :
() = Inv.inv
def Equiv.inv (G : Type u_10) [] :

Inversion on a Group or GroupWithZero is a permutation of the underlying type.

Equations
Instances For
@[simp]
theorem Equiv.neg_symm {G : Type u_10} [] :
().symm =
@[simp]
theorem Equiv.inv_symm {G : Type u_10} [] :
().symm =