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

Equiv, MulEquiv, AddEquiv

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

Make a ZeroHom inverse from the bijective inverse of a ZeroHom

Equations

• ZeroHom.inverse f g h₁ = { toFun := g, map_zero' := ⋯ }

theorem ZeroHom.inverse.proof_1 {M : Type u_1} {N : Type u_2} [Zero M] [Zero N] (f : ZeroHom M N) (g : N → M) (h₁ : Function.LeftInverse g ⇑f) : 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 : N → M) (h₁ : Function.LeftInverse g ⇑f) : ∀ (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 : N → M) (h₁ : Function.LeftInverse g ⇑f) : ∀ (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 : N → M) (h₁ : Function.LeftInverse g ⇑f) : OneHom N M

Makes a OneHom inverse from the bijective inverse of a OneHom

Equations

• OneHom.inverse f g h₁ = { toFun := g, map_one' := ⋯ }

def AddHom.inverse {M : Type u_6} {N : Type u_7} [Add M] [Add N] (f : AddHom M N) (g : N → M) (h₁ : Function.LeftInverse g ⇑f) (h₂ : Function.RightInverse g ⇑f) : AddHom N M

Makes an additive inverse from a bijection which preserves addition.

Equations

• AddHom.inverse f g h₁ h₂ = { toFun := g, map_add' := ⋯ }

theorem AddHom.inverse.proof_1 {M : Type u_1} {N : Type u_2} [Add M] [Add N] (f : AddHom M N) (g : N → M) (h₁ : Function.LeftInverse g ⇑f) (h₂ : Function.RightInverse g ⇑f) (x : N) (y : N) : g (x + y) = g x + g y

@[simp]

theorem AddHom.inverse_apply {M : Type u_6} {N : Type u_7} [Add M] [Add N] (f : AddHom M N) (g : N → M) (h₁ : Function.LeftInverse g ⇑f) (h₂ : Function.RightInverse g ⇑f) : ∀ (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 : N → M) (h₁ : Function.LeftInverse g ⇑f) (h₂ : Function.RightInverse g ⇑f) : ∀ (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 : N → M) (h₁ : Function.LeftInverse g ⇑f) (h₂ : Function.RightInverse g ⇑f) : N →ₙ* M

Makes a multiplicative inverse from a bijection which preserves multiplication.

Equations

• MulHom.inverse f g h₁ h₂ = { toFun := g, map_mul' := ⋯ }

theorem AddMonoidHom.inverse.proof_3 {A : Type u_1} {B : Type u_2} [AddMonoid A] [AddMonoid B] (f : A →+ B) (g : B → A) (h₁ : Function.LeftInverse g ⇑f) : (ZeroHom.inverse (↑f) g h₁).toFun 0 = 0

theorem AddMonoidHom.inverse.proof_4 {A : Type u_1} {B : Type u_2} [AddMonoid A] [AddMonoid B] (f : A →+ B) (g : B → A) (h₁ : Function.LeftInverse g ⇑f) (h₂ : Function.RightInverse g ⇑f) (x : B) (y : B) : (AddHom.inverse (↑f) g h₁ h₂).toFun (x + y) = (AddHom.inverse (↑f) g h₁ h₂).toFun x + (AddHom.inverse (↑f) g h₁ h₂).toFun y

theorem AddMonoidHom.inverse.proof_1 {A : Type u_2} {B : Type u_1} [AddMonoid A] [AddMonoid B] : ZeroHomClass (A →+ B) A B

def AddMonoidHom.inverse {A : Type u_12} {B : Type u_13} [AddMonoid A] [AddMonoid B] (f : A →+ B) (g : B → A) (h₁ : Function.LeftInverse g ⇑f) (h₂ : Function.RightInverse g ⇑f) : B →+ A

The inverse of a bijective AddMonoidHom is an AddMonoidHom.

Equations

• AddMonoidHom.inverse f g h₁ h₂ = let __src := ZeroHom.inverse (↑f) g h₁; let __src := AddHom.inverse (↑f) g h₁ h₂; { toZeroHom := { toFun := g, map_zero' := ⋯ }, map_add' := ⋯ }

theorem AddMonoidHom.inverse.proof_2 {A : Type u_2} {B : Type u_1} [AddMonoid A] [AddMonoid B] : AddHomClass (A →+ B) A B

@[simp]

theorem AddMonoidHom.inverse_apply {A : Type u_12} {B : Type u_13} [AddMonoid A] [AddMonoid B] (f : A →+ B) (g : B → A) (h₁ : Function.LeftInverse g ⇑f) (h₂ : Function.RightInverse g ⇑f) : ∀ (a : B), (AddMonoidHom.inverse f g h₁ h₂) a = g a

@[simp]

theorem MonoidHom.inverse_apply {A : Type u_12} {B : Type u_13} [Monoid A] [Monoid B] (f : A →* B) (g : B → A) (h₁ : Function.LeftInverse g ⇑f) (h₂ : Function.RightInverse g ⇑f) : ∀ (a : B), (MonoidHom.inverse f g h₁ h₂) a = g a

def MonoidHom.inverse {A : Type u_12} {B : Type u_13} [Monoid A] [Monoid B] (f : A →* B) (g : B → A) (h₁ : Function.LeftInverse g ⇑f) (h₂ : Function.RightInverse g ⇑f) : B →* A

The inverse of a bijective MonoidHom is a MonoidHom.

Equations

• MonoidHom.inverse f g h₁ h₂ = let __src := OneHom.inverse (↑f) g h₁; let __src := MulHom.inverse (↑f) g h₁ h₂; { toOneHom := { toFun := g, map_one' := ⋯ }, map_mul' := ⋯ }

structure AddEquiv (A : Type u_12) (B : Type u_13) [Add A] [Add B] extends Equiv : Type (max u_12 u_13)

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

• toFun : A → B
• invFun : B → A
• left_inv : Function.LeftInverse self.invFun self.toFun
• right_inv : Function.RightInverse self.invFun self.toFun
• map_add' : ∀ (x y : A), self.toFun (x + y) = self.toFun x + self.toFun y

  The proposition that the function preserves addition

class AddEquivClass (F : Type u_12) (A : outParam (Type u_13)) (B : outParam (Type u_14)) [Add A] [Add B] [EquivLike F A B] : Prop

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

• map_add : ∀ (f : F) (a b : A), f (a + b) = f a + f b

  Preserves addition.

@[reducible]

abbrev AddEquiv.toAddHom {A : Type u_12} {B : Type u_13} [Add A] [Add B] (self : A ≃+ B) : AddHom A B

The AddHom underlying an AddEquiv.

Equations

• AddEquiv.toAddHom self = { toFun := self.toFun, map_add' := ⋯ }

structure MulEquiv (M : Type u_12) (N : Type u_13) [Mul M] [Mul N] extends Equiv : Type (max u_12 u_13)

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

• toFun : M → N
• invFun : N → M
• left_inv : Function.LeftInverse self.invFun self.toFun
• right_inv : Function.RightInverse self.invFun self.toFun
• map_mul' : ∀ (x y : M), self.toFun (x * y) = self.toFun x * self.toFun y

  The proposition that the function preserves multiplication

@[reducible]

abbrev MulEquiv.toMulHom {M : Type u_12} {N : Type u_13} [Mul M] [Mul N] (self : M ≃* N) : M →ₙ* N

The MulHom underlying a MulEquiv.

Equations

• MulEquiv.toMulHom self = { toFun := self.toFun, map_mul' := ⋯ }

class MulEquivClass (F : Type u_12) (A : outParam (Type u_13)) (B : outParam (Type u_14)) [Mul A] [Mul B] [EquivLike F A B] : Prop

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

• map_mul : ∀ (f : F) (a b : A), f (a * b) = f a * f b

  Preserves multiplication.

def «term_≃*_» : Lean.TrailingParserDescr

Notation for a MulEquiv.

Equations

• «term_≃*_» = Lean.ParserDescr.trailingNode `term_≃*_ 25 25 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≃* ") (Lean.ParserDescr.cat `term 26))

def «term_≃+_» : Lean.TrailingParserDescr

Notation for an AddEquiv.

Equations

• «term_≃+_» = Lean.ParserDescr.trailingNode `term_≃+_ 25 25 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≃+ ") (Lean.ParserDescr.cat `term 26))

instance AddEquivClass.instAddHomClass {M : Type u_6} {N : Type u_7} (F : Type u_12) [Add M] [Add N] [EquivLike F M N] [h : AddEquivClass F M N] : AddHomClass F M N

Equations

• ⋯ = ⋯

instance MulEquivClass.instMulHomClass {M : Type u_6} {N : Type u_7} (F : Type u_12) [Mul M] [Mul N] [EquivLike F M N] [h : MulEquivClass F M N] : MulHomClass F M N

Equations

• ⋯ = ⋯

instance AddEquivClass.instAddMonoidHomClass (F : Type u_1) {M : Type u_6} {N : Type u_7} [EquivLike F M N] [AddZeroClass M] [AddZeroClass N] [AddEquivClass F M N] : AddMonoidHomClass F M N

Equations

• ⋯ = ⋯

instance MulEquivClass.instMonoidHomClass (F : Type u_1) {M : Type u_6} {N : Type u_7} [EquivLike F M N] [MulOneClass M] [MulOneClass N] [MulEquivClass F M N] : MonoidHomClass F M N

Equations

• ⋯ = ⋯

@[simp]

theorem AddEquivClass.map_eq_zero_iff {F : Type u_1} {M : Type u_12} {N : Type u_13} [AddZeroClass M] [AddZeroClass N] [EquivLike F M N] [AddEquivClass F M N] (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} [MulOneClass M] [MulOneClass N] [EquivLike F M N] [MulEquivClass F M N] (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} [AddZeroClass M] [AddZeroClass N] [EquivLike F M N] [AddEquivClass F M N] (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} [MulOneClass M] [MulOneClass N] [EquivLike F M N] [MulEquivClass F M N] (h : F) {x : M} : h x ≠ 1 ↔ x ≠ 1

def AddEquivClass.toAddEquiv {F : Type u_1} {α : Type u_2} {β : Type u_3} [EquivLike F α β] [Add α] [Add β] [AddEquivClass F α β] (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

• ↑f = let __src := ↑f; let __src_1 := ↑f; { toEquiv := __src, map_add' := ⋯ }

def MulEquivClass.toMulEquiv {F : Type u_1} {α : Type u_2} {β : Type u_3} [EquivLike F α β] [Mul α] [Mul β] [MulEquivClass F α β] (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

• ↑f = let __src := ↑f; let __src_1 := ↑f; { toEquiv := __src, map_mul' := ⋯ }

instance instCoeTCAddEquiv {F : Type u_1} {α : Type u_2} {β : Type u_3} [EquivLike F α β] [Add α] [Add β] [AddEquivClass F α β] : CoeTC F (α ≃+ β)

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

Equations

• instCoeTCAddEquiv = { coe := AddEquivClass.toAddEquiv }

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

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

Equations

• instCoeTCMulEquiv = { coe := MulEquivClass.toMulEquiv }

theorem AddEquivClass.toAddEquiv_injective {F : Type u_1} {α : Type u_2} {β : Type u_3} [EquivLike F α β] [Add α] [Add β] [AddEquivClass F α β] : Function.Injective AddEquivClass.toAddEquiv

theorem MulEquivClass.toMulEquiv_injective {F : Type u_1} {α : Type u_2} {β : Type u_3} [EquivLike F α β] [Mul α] [Mul β] [MulEquivClass F α β] : Function.Injective MulEquivClass.toMulEquiv

theorem AddEquiv.instEquivLikeAddEquiv.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

theorem AddEquiv.instEquivLikeAddEquiv.proof_2 {M : Type u_2} {N : Type u_1} [Add M] [Add N] (f : M ≃+ N) : Function.RightInverse f.invFun f.toFun

theorem AddEquiv.instEquivLikeAddEquiv.proof_1 {M : Type u_2} {N : Type u_1} [Add M] [Add N] (f : M ≃+ N) : Function.LeftInverse f.invFun f.toFun

instance AddEquiv.instEquivLikeAddEquiv {M : Type u_6} {N : Type u_7} [Add M] [Add N] : EquivLike (M ≃+ N) M N

Equations

• AddEquiv.instEquivLikeAddEquiv = { coe := fun (f : M ≃+ N) => f.toFun, inv := fun (f : M ≃+ N) => f.invFun, left_inv := ⋯, right_inv := ⋯, coe_injective' := ⋯ }

instance MulEquiv.instEquivLikeMulEquiv {M : Type u_6} {N : Type u_7} [Mul M] [Mul N] : EquivLike (M ≃* N) M N

Equations

• MulEquiv.instEquivLikeMulEquiv = { coe := fun (f : M ≃* N) => f.toFun, inv := fun (f : M ≃* N) => f.invFun, left_inv := ⋯, right_inv := ⋯, coe_injective' := ⋯ }

instance AddEquiv.instAddEquivClassAddEquivInstEquivLikeAddEquiv {M : Type u_6} {N : Type u_7} [Add M] [Add N] : AddEquivClass (M ≃+ N) M N

Equations

• ⋯ = ⋯

instance MulEquiv.instMulEquivClassMulEquivInstEquivLikeMulEquiv {M : Type u_6} {N : Type u_7} [Mul M] [Mul N] : MulEquivClass (M ≃* N) M N

Equations

• ⋯ = ⋯

instance AddEquiv.instCoeFunAddEquivForAll {M : Type u_6} {N : Type u_7} [Add M] [Add N] : CoeFun (M ≃+ N) fun (x : M ≃+ N) => M → N

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) => M → N

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]

theorem AddEquiv.toAddHom_eq_coe {M : Type u_6} {N : Type u_7} [Add M] [Add N] (f : M ≃+ N) : AddEquiv.toAddHom f = ↑f

@[simp]

theorem MulEquiv.toMulHom_eq_coe {M : Type u_6} {N : Type u_7} [Mul M] [Mul N] (f : M ≃* N) : MulEquiv.toMulHom f = ↑f

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

theorem AddEquiv.coe_toAddHom {M : Type u_6} {N : Type u_7} [Add M] [Add N] {f : M ≃+ N} : ⇑(AddEquiv.toAddHom f) = ⇑f

@[simp]

theorem MulEquiv.coe_toMulHom {M : Type u_6} {N : Type u_7} [Mul M] [Mul N] {f : M ≃* N} : ⇑(MulEquiv.toMulHom f) = ⇑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

An additive isomorphism preserves addition.

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

Makes an additive isomorphism from a bijection which preserves addition.

Equations

• AddEquiv.mk' f h = { toEquiv := f, map_add' := h }

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

• MulEquiv.mk' f h = { toEquiv := f, map_mul' := h }

theorem AddEquiv.bijective {M : Type u_6} {N : Type u_7} [Add M] [Add N] (e : M ≃+ N) : Function.Bijective ⇑e

theorem MulEquiv.bijective {M : Type u_6} {N : Type u_7} [Mul M] [Mul N] (e : M ≃* N) : Function.Bijective ⇑e

theorem AddEquiv.injective {M : Type u_6} {N : Type u_7} [Add M] [Add N] (e : M ≃+ N) : Function.Injective ⇑e

theorem MulEquiv.injective {M : Type u_6} {N : Type u_7} [Mul M] [Mul N] (e : M ≃* N) : Function.Injective ⇑e

theorem AddEquiv.surjective {M : Type u_6} {N : Type u_7} [Add M] [Add N] (e : M ≃+ N) : Function.Surjective ⇑e

theorem MulEquiv.surjective {M : Type u_6} {N : Type u_7} [Mul M] [Mul N] (e : M ≃* N) : Function.Surjective ⇑e

def AddEquiv.refl (M : Type u_12) [Add M] : M ≃+ M

The identity map is an additive isomorphism.

Equations

• AddEquiv.refl M = let __src := Equiv.refl M; { toEquiv := __src, map_add' := ⋯ }

theorem AddEquiv.refl.proof_1 (M : Type u_1) [Add M] : ∀ (x x_1 : M), (Equiv.refl M).toFun (x + x_1) = (Equiv.refl M).toFun (x + x_1)

def MulEquiv.refl (M : Type u_12) [Mul M] : M ≃* M

The identity map is a multiplicative isomorphism.

Equations

• MulEquiv.refl M = let __src := Equiv.refl M; { toEquiv := __src, map_mul' := ⋯ }

instance AddEquiv.instInhabitedAddEquiv {M : Type u_6} [Add M] : Inhabited (M ≃+ M)

Equations

• AddEquiv.instInhabitedAddEquiv = { default := AddEquiv.refl M }

instance MulEquiv.instInhabitedMulEquiv {M : Type u_6} [Mul M] : Inhabited (M ≃* M)

Equations

• MulEquiv.instInhabitedMulEquiv = { default := MulEquiv.refl M }

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

• AddEquiv.symm h = { toEquiv := h.symm, map_add' := ⋯ }

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

• MulEquiv.symm h = { toEquiv := h.symm, map_mul' := ⋯ }

theorem AddEquiv.invFun_eq_symm {M : Type u_6} {N : Type u_7} [Add M] [Add N] {f : M ≃+ N} : f.invFun = ⇑(AddEquiv.symm f)

theorem MulEquiv.invFun_eq_symm {M : Type u_6} {N : Type u_7} [Mul M] [Mul N] {f : M ≃* N} : f.invFun = ⇑(MulEquiv.symm f)

@[simp]

theorem AddEquiv.coe_toEquiv_symm {M : Type u_6} {N : Type u_7} [Add M] [Add N] (f : M ≃+ N) : ⇑(↑f).symm = ⇑(AddEquiv.symm f)

@[simp]

theorem MulEquiv.coe_toEquiv_symm {M : Type u_6} {N : Type u_7} [Mul M] [Mul N] (f : M ≃* N) : ⇑(↑f).symm = ⇑(MulEquiv.symm f)

@[simp]

theorem AddEquiv.equivLike_neg_eq_symm {M : Type u_6} {N : Type u_7} [Add M] [Add N] (f : M ≃+ N) : EquivLike.inv f = ⇑(AddEquiv.symm f)

@[simp]

theorem MulEquiv.equivLike_inv_eq_symm {M : Type u_6} {N : Type u_7} [Mul M] [Mul N] (f : M ≃* N) : EquivLike.inv f = ⇑(MulEquiv.symm f)

def AddEquiv.Simps.symm_apply {M : Type u_6} {N : Type u_7} [Add M] [Add N] (e : M ≃+ N) : N → M

See Note [custom simps projection]

Equations

• AddEquiv.Simps.symm_apply e = ⇑(AddEquiv.symm e)

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

See Note [custom simps projection]

Equations

• MulEquiv.Simps.symm_apply e = ⇑(MulEquiv.symm e)

@[simp]

theorem AddEquiv.toEquiv_symm {M : Type u_6} {N : Type u_7} [Add M] [Add N] (f : M ≃+ N) : ↑(AddEquiv.symm f) = (↑f).symm

@[simp]

theorem MulEquiv.toEquiv_symm {M : Type u_6} {N : Type u_7} [Mul M] [Mul N] (f : M ≃* N) : ↑(MulEquiv.symm f) = (↑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) : AddEquiv.symm (AddEquiv.symm f) = f

@[simp]

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

theorem AddEquiv.symm_bijective {M : Type u_6} {N : Type u_7} [Add M] [Add N] : Function.Bijective AddEquiv.symm

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), f.toFun (x + y) = f.toFun x + f.toFun y) : AddEquiv.symm { toEquiv := f, map_add' := h } = { toEquiv := f.symm, map_add' := ⋯ }

@[simp]

theorem MulEquiv.symm_mk {M : Type u_6} {N : Type u_7} [Mul M] [Mul N] (f : M ≃ N) (h : ∀ (x y : M), f.toFun (x * y) = f.toFun x * f.toFun y) : MulEquiv.symm { toEquiv := f, map_mul' := h } = { toEquiv := f.symm, map_mul' := ⋯ }

@[simp]

theorem AddEquiv.refl_symm {M : Type u_6} [Add M] : AddEquiv.symm (AddEquiv.refl M) = AddEquiv.refl M

@[simp]

theorem MulEquiv.refl_symm {M : Type u_6} [Mul M] : MulEquiv.symm (MulEquiv.refl M) = MulEquiv.refl M

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

Transitivity of addition-preserving isomorphisms

Equations

• AddEquiv.trans h1 h2 = let __src := h1.trans h2.toEquiv; { toEquiv := __src, map_add' := ⋯ }

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

• MulEquiv.trans h1 h2 = let __src := h1.trans h2.toEquiv; { toEquiv := __src, map_mul' := ⋯ }

@[simp]

theorem AddEquiv.apply_symm_apply {M : Type u_6} {N : Type u_7} [Add M] [Add N] (e : M ≃+ N) (y : N) : e ((AddEquiv.symm 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 ((MulEquiv.symm 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) : (AddEquiv.symm e) (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) : (MulEquiv.symm e) (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) : ⇑(AddEquiv.symm e) ∘ ⇑e = id

@[simp]

theorem MulEquiv.symm_comp_self {M : Type u_6} {N : Type u_7} [Mul M] [Mul N] (e : M ≃* N) : ⇑(MulEquiv.symm e) ∘ ⇑e = id

@[simp]

theorem AddEquiv.self_comp_symm {M : Type u_6} {N : Type u_7} [Add M] [Add N] (e : M ≃+ N) : ⇑e ∘ ⇑(AddEquiv.symm e) = id

@[simp]

theorem MulEquiv.self_comp_symm {M : Type u_6} {N : Type u_7} [Mul M] [Mul N] (e : M ≃* N) : ⇑e ∘ ⇑(MulEquiv.symm e) = id

@[simp]

theorem AddEquiv.coe_refl {M : Type u_6} [Add M] : ⇑(AddEquiv.refl M) = id

@[simp]

theorem MulEquiv.coe_refl {M : Type u_6} [Mul M] : ⇑(MulEquiv.refl M) = id

@[simp]

theorem AddEquiv.refl_apply {M : Type u_6} [Add M] (m : M) : (AddEquiv.refl M) m = m

@[simp]

theorem MulEquiv.refl_apply {M : Type u_6} [Mul M] (m : M) : (MulEquiv.refl 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) : (AddEquiv.symm (AddEquiv.trans e₁ e₂)) p = (AddEquiv.symm e₁) ((AddEquiv.symm e₂) 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 = (MulEquiv.symm e₁) ((MulEquiv.symm e₂) 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 = (AddEquiv.symm e) 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 = (MulEquiv.symm e) 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} : (AddEquiv.symm e) 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} : (MulEquiv.symm e) 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 = (AddEquiv.symm e) 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 = (MulEquiv.symm e) 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 ∘ ⇑(AddEquiv.symm e) ↔ 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 ∘ ⇑(MulEquiv.symm e) ↔ 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 ∘ ⇑(AddEquiv.symm e) = 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 ∘ ⇑(MulEquiv.symm e) = 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 = ⇑(AddEquiv.symm e) ∘ 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 = ⇑(MulEquiv.symm e) ∘ 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) : ⇑(AddEquiv.symm e) ∘ 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) : ⇑(MulEquiv.symm e) ∘ 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) : AddEquiv.trans (AddEquiv.symm e) e = AddEquiv.refl N

@[simp]

theorem MulEquiv.symm_trans_self {M : Type u_6} {N : Type u_7} [Mul M] [Mul N] (e : M ≃* N) : MulEquiv.trans (MulEquiv.symm e) e = MulEquiv.refl N

@[simp]

theorem AddEquiv.self_trans_symm {M : Type u_6} {N : Type u_7} [Add M] [Add N] (e : M ≃+ N) : AddEquiv.trans e (AddEquiv.symm e) = AddEquiv.refl M

@[simp]

theorem MulEquiv.self_trans_symm {M : Type u_6} {N : Type u_7} [Mul M] [Mul N] (e : M ≃* N) : MulEquiv.trans e (MulEquiv.symm e) = MulEquiv.refl M

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' : N → M) (h₁ : Function.LeftInverse e' ⇑e) (h₂ : Function.RightInverse e' ⇑e) (h₃ : ∀ (x y : M), { toFun := ⇑e, invFun := e', left_inv := h₁, right_inv := h₂ }.toFun (x + y) = { toFun := ⇑e, invFun := e', left_inv := h₁, right_inv := h₂ }.toFun x + { toFun := ⇑e, invFun := e', left_inv := h₁, right_inv := h₂ }.toFun 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' : N → M) (h₁ : Function.LeftInverse e' ⇑e) (h₂ : Function.RightInverse e' ⇑e) (h₃ : ∀ (x y : M), { toFun := ⇑e, invFun := e', left_inv := h₁, right_inv := h₂ }.toFun (x * y) = { toFun := ⇑e, invFun := e', left_inv := h₁, right_inv := h₂ }.toFun x * { toFun := ⇑e, invFun := e', left_inv := h₁, right_inv := h₂ }.toFun 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 : N → M) (h₁ : Function.LeftInverse (⇑e) f) (h₂ : Function.RightInverse (⇑e) f) (h₃ : ∀ (x y : N), { toFun := f, invFun := ⇑e, left_inv := h₁, right_inv := h₂ }.toFun (x + y) = { toFun := f, invFun := ⇑e, left_inv := h₁, right_inv := h₂ }.toFun x + { toFun := f, invFun := ⇑e, left_inv := h₁, right_inv := h₂ }.toFun y) : { toEquiv := { toFun := f, invFun := ⇑e, left_inv := h₁, right_inv := h₂ }, map_add' := h₃ } = AddEquiv.symm e

@[simp]

theorem MulEquiv.mk_coe' {M : Type u_6} {N : Type u_7} [Mul M] [Mul N] (e : M ≃* N) (f : N → M) (h₁ : Function.LeftInverse (⇑e) f) (h₂ : Function.RightInverse (⇑e) f) (h₃ : ∀ (x y : N), { toFun := f, invFun := ⇑e, left_inv := h₁, right_inv := h₂ }.toFun (x * y) = { toFun := f, invFun := ⇑e, left_inv := h₁, right_inv := h₂ }.toFun x * { toFun := f, invFun := ⇑e, left_inv := h₁, right_inv := h₂ }.toFun y) : { toEquiv := { toFun := f, invFun := ⇑e, left_inv := h₁, right_inv := h₂ }, map_mul' := h₃ } = MulEquiv.symm e

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

theorem AddEquiv.addEquivOfUnique.proof_1 {M : Type u_2} {N : Type u_1} [Unique M] [Unique N] [Add M] [Add N] : ∀ (x x_1 : M), (Equiv.equivOfUnique M N).toFun (x + x_1) = (Equiv.equivOfUnique M N).toFun x + (Equiv.equivOfUnique M N).toFun x_1

def AddEquiv.addEquivOfUnique {M : Type u_12} {N : Type u_13} [Unique M] [Unique N] [Add M] [Add N] : M ≃+ N

The AddEquiv between two AddMonoids with a unique element.

Equations

• AddEquiv.addEquivOfUnique = let __src := Equiv.equivOfUnique M N; { toEquiv := __src, map_add' := ⋯ }

def MulEquiv.mulEquivOfUnique {M : Type u_12} {N : Type u_13} [Unique M] [Unique N] [Mul M] [Mul N] : M ≃* N

The MulEquiv between two monoids with a unique element.

Equations

• MulEquiv.mulEquivOfUnique = let __src := Equiv.equivOfUnique M N; { toEquiv := __src, map_mul' := ⋯ }

instance AddEquiv.instUniqueAddEquiv {M : Type u_12} {N : Type u_13} [Unique M] [Unique N] [Add M] [Add N] : 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 := ⋯ }

theorem AddEquiv.instUniqueAddEquiv.proof_1 {M : Type u_2} {N : Type u_1} [Unique M] [Unique N] [Add M] [Add N] : ∀ (x : M ≃+ N), x = default

instance MulEquiv.instUniqueMulEquiv {M : Type u_12} {N : Type u_13} [Unique M] [Unique N] [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 := ⋯ }

Monoids

theorem AddEquiv.coe_addMonoidHom_refl {M : Type u_6} [AddZeroClass M] : ↑(AddEquiv.refl M) = AddMonoidHom.id M

theorem MulEquiv.coe_monoidHom_refl {M : Type u_6} [MulOneClass M] : ↑(MulEquiv.refl M) = MonoidHom.id M

theorem AddEquiv.coe_addMonoidHom_trans {M : Type u_6} {N : Type u_7} {P : Type u_8} [AddZeroClass M] [AddZeroClass N] [AddZeroClass P] (e₁ : M ≃+ N) (e₂ : N ≃+ P) : ↑(AddEquiv.trans e₁ e₂) = AddMonoidHom.comp ↑e₂ ↑e₁

theorem MulEquiv.coe_monoidHom_trans {M : Type u_6} {N : Type u_7} {P : Type u_8} [MulOneClass M] [MulOneClass N] [MulOneClass P] (e₁ : M ≃* N) (e₂ : N ≃* P) : ↑(MulEquiv.trans e₁ e₂) = MonoidHom.comp ↑e₂ ↑e₁

@[simp]

theorem AddEquiv.coe_addMonoidHom_comp_coe_addMonoidHom_symm {M : Type u_6} {N : Type u_7} [AddZeroClass M] [AddZeroClass N] (e : M ≃+ N) : AddMonoidHom.comp ↑e ↑(AddEquiv.symm e) = AddMonoidHom.id N

@[simp]

theorem MulEquiv.coe_monoidHom_comp_coe_monoidHom_symm {M : Type u_6} {N : Type u_7} [MulOneClass M] [MulOneClass N] (e : M ≃* N) : MonoidHom.comp ↑e ↑(MulEquiv.symm e) = MonoidHom.id N

@[simp]

theorem AddEquiv.coe_addMonoidHom_symm_comp_coe_addMonoidHom {M : Type u_6} {N : Type u_7} [AddZeroClass M] [AddZeroClass N] (e : M ≃+ N) : AddMonoidHom.comp ↑(AddEquiv.symm e) ↑e = AddMonoidHom.id M

@[simp]

theorem MulEquiv.coe_monoidHom_symm_comp_coe_monoidHom {M : Type u_6} {N : Type u_7} [MulOneClass M] [MulOneClass N] (e : M ≃* N) : MonoidHom.comp ↑(MulEquiv.symm e) ↑e = MonoidHom.id M

theorem AddEquiv.comp_left_injective {M : Type u_6} {N : Type u_7} {P : Type u_8} [AddZeroClass M] [AddZeroClass N] [AddZeroClass P] (e : M ≃+ N) : Function.Injective fun (f : N →+ P) => AddMonoidHom.comp f ↑e

theorem MulEquiv.comp_left_injective {M : Type u_6} {N : Type u_7} {P : Type u_8} [MulOneClass M] [MulOneClass N] [MulOneClass P] (e : M ≃* N) : Function.Injective fun (f : N →* P) => MonoidHom.comp f ↑e

theorem AddEquiv.comp_right_injective {M : Type u_6} {N : Type u_7} {P : Type u_8} [AddZeroClass M] [AddZeroClass N] [AddZeroClass P] (e : M ≃+ N) : Function.Injective fun (f : P →+ M) => AddMonoidHom.comp (↑e) f

theorem MulEquiv.comp_right_injective {M : Type u_6} {N : Type u_7} {P : Type u_8} [MulOneClass M] [MulOneClass N] [MulOneClass P] (e : M ≃* N) : Function.Injective fun (f : P →* M) => MonoidHom.comp (↑e) f

theorem AddEquiv.map_zero {M : Type u_6} {N : Type u_7} [AddZeroClass M] [AddZeroClass N] (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_6} {N : Type u_7} [MulOneClass M] [MulOneClass N] (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_6} {N : Type u_7} [AddZeroClass M] [AddZeroClass N] (h : M ≃+ N) {x : M} : h x = 0 ↔ x = 0

theorem MulEquiv.map_eq_one_iff {M : Type u_6} {N : Type u_7} [MulOneClass M] [MulOneClass N] (h : M ≃* N) {x : M} : h x = 1 ↔ x = 1

theorem AddEquiv.map_ne_zero_iff {M : Type u_6} {N : Type u_7} [AddZeroClass M] [AddZeroClass N] (h : M ≃+ N) {x : M} : h x ≠ 0 ↔ x ≠ 0

theorem MulEquiv.map_ne_one_iff {M : Type u_6} {N : Type u_7} [MulOneClass M] [MulOneClass N] (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] [FunLike F M N] [AddHomClass F M N] (f : F) (hf : Function.Bijective ⇑f) : M ≃+ N

A bijective AddSemigroup homomorphism is an isomorphism

Equations

• AddEquiv.ofBijective f hf = let __src := Equiv.ofBijective (⇑f) hf; { toEquiv := __src, map_add' := ⋯ }

@[simp]

theorem MulEquiv.ofBijective_apply {M : Type u_12} {N : Type u_13} {F : Type u_14} [Mul M] [Mul N] [FunLike F M N] [MulHomClass F M N] (f : F) (hf : Function.Bijective ⇑f) (a : M) : (MulEquiv.ofBijective f hf) a = f a

@[simp]

theorem AddEquiv.ofBijective_apply {M : Type u_12} {N : Type u_13} {F : Type u_14} [Add M] [Add N] [FunLike F M N] [AddHomClass F M N] (f : F) (hf : Function.Bijective ⇑f) (a : M) : (AddEquiv.ofBijective f hf) a = f a

noncomputable def MulEquiv.ofBijective {M : Type u_12} {N : Type u_13} {F : Type u_14} [Mul M] [Mul N] [FunLike F M N] [MulHomClass F M N] (f : F) (hf : Function.Bijective ⇑f) : M ≃* N

A bijective Semigroup homomorphism is an isomorphism

Equations

• MulEquiv.ofBijective f hf = let __src := Equiv.ofBijective (⇑f) hf; { toEquiv := __src, map_mul' := ⋯ }

@[simp]

theorem AddEquiv.ofBijective_apply_symm_apply {M : Type u_6} {N : Type u_7} [AddZeroClass M] [AddZeroClass N] {n : N} (f : M →+ N) (hf : Function.Bijective ⇑f) : f ((AddEquiv.symm (AddEquiv.ofBijective f hf)) n) = n

@[simp]

theorem MulEquiv.ofBijective_apply_symm_apply {M : Type u_6} {N : Type u_7} [MulOneClass M] [MulOneClass N] {n : N} (f : M →* N) (hf : Function.Bijective ⇑f) : f ((MulEquiv.symm (MulEquiv.ofBijective f hf)) n) = n

def AddEquiv.toAddMonoidHom {M : Type u_6} {N : Type u_7} [AddZeroClass M] [AddZeroClass N] (h : M ≃+ N) : M →+ N

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

Equations

• AddEquiv.toAddMonoidHom h = { toZeroHom := { toFun := h.toFun, map_zero' := ⋯ }, map_add' := ⋯ }

theorem AddEquiv.toAddMonoidHom.proof_1 {M : Type u_2} {N : Type u_1} [AddZeroClass M] [AddZeroClass N] (h : M ≃+ N) (x : M) (y : M) : h.toFun (x + y) = h.toFun x + h.toFun y

def MulEquiv.toMonoidHom {M : Type u_6} {N : Type u_7} [MulOneClass M] [MulOneClass N] (h : M ≃* N) : M →* N

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

Equations

• MulEquiv.toMonoidHom h = { toOneHom := { toFun := h.toFun, map_one' := ⋯ }, map_mul' := ⋯ }

@[simp]

theorem AddEquiv.coe_toAddMonoidHom {M : Type u_6} {N : Type u_7} [AddZeroClass M] [AddZeroClass N] (e : M ≃+ N) : ⇑(AddEquiv.toAddMonoidHom e) = ⇑e

@[simp]

theorem MulEquiv.coe_toMonoidHom {M : Type u_6} {N : Type u_7} [MulOneClass M] [MulOneClass N] (e : M ≃* N) : ⇑(MulEquiv.toMonoidHom e) = ⇑e

theorem AddEquiv.toAddMonoidHom_injective {M : Type u_6} {N : Type u_7} [AddZeroClass M] [AddZeroClass N] : Function.Injective AddEquiv.toAddMonoidHom

theorem MulEquiv.toMonoidHom_injective {M : Type u_6} {N : Type u_7} [MulOneClass M] [MulOneClass N] : Function.Injective MulEquiv.toMonoidHom

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 : M → P) (k : M → P) : { toFun := fun (h : M → P) (n : N) => g (h (f.symm n)), invFun := fun (k : N → Q) (m : M) => (AddEquiv.symm g) (k (f m)), left_inv := ⋯, right_inv := ⋯ }.toFun (h + k) = { toFun := fun (h : M → P) (n : N) => g (h (f.symm n)), invFun := fun (k : N → Q) (m : M) => (AddEquiv.symm g) (k (f m)), left_inv := ⋯, right_inv := ⋯ }.toFun h + { toFun := fun (h : M → P) (n : N) => g (h (f.symm n)), invFun := fun (k : N → Q) (m : M) => (AddEquiv.symm g) (k (f m)), left_inv := ⋯, right_inv := ⋯ }.toFun k

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 : M → P) : (fun (k : N → Q) (m : M) => (AddEquiv.symm g) (k (f m))) ((fun (h : M → P) (n : N) => g (h (f.symm n))) h) = h

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) : (M → P) ≃+ (N → Q)

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.

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 : N → Q) : (fun (h : M → P) (n : N) => g (h (f.symm n))) ((fun (k : N → Q) (m : M) => (AddEquiv.symm g) (k (f m))) 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 : M → P) (n : N) : (AddEquiv.arrowCongr f g) 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 : M → P) (n : N) : (MulEquiv.arrowCongr f g) 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) : (M → P) ≃* (N → Q)

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.

theorem AddEquiv.addMonoidHomCongr.proof_2 {M : Type u_4} {N : Type u_2} {P : Type u_3} {Q : Type u_1} [AddZeroClass M] [AddZeroClass N] [AddCommMonoid P] [AddCommMonoid Q] (f : M ≃+ N) (g : P ≃+ Q) (k : N →+ Q) : (fun (h : M →+ P) => AddMonoidHom.comp (AddEquiv.toAddMonoidHom g) (AddMonoidHom.comp h (AddEquiv.toAddMonoidHom (AddEquiv.symm f)))) ((fun (k : N →+ Q) => AddMonoidHom.comp (AddEquiv.toAddMonoidHom (AddEquiv.symm g)) (AddMonoidHom.comp k (AddEquiv.toAddMonoidHom f))) k) = k

def AddEquiv.addMonoidHomCongr {M : Type u_12} {N : Type u_13} {P : Type u_14} {Q : Type u_15} [AddZeroClass M] [AddZeroClass N] [AddCommMonoid P] [AddCommMonoid Q] (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.

theorem AddEquiv.addMonoidHomCongr.proof_3 {M : Type u_2} {N : Type u_3} {P : Type u_1} {Q : Type u_4} [AddZeroClass M] [AddZeroClass N] [AddCommMonoid P] [AddCommMonoid Q] (f : M ≃+ N) (g : P ≃+ Q) (h : M →+ P) (k : M →+ P) : { toFun := fun (h : M →+ P) => AddMonoidHom.comp (AddEquiv.toAddMonoidHom g) (AddMonoidHom.comp h (AddEquiv.toAddMonoidHom (AddEquiv.symm f))), invFun := fun (k : N →+ Q) => AddMonoidHom.comp (AddEquiv.toAddMonoidHom (AddEquiv.symm g)) (AddMonoidHom.comp k (AddEquiv.toAddMonoidHom f)), left_inv := ⋯, right_inv := ⋯ }.toFun (h + k) = { toFun := fun (h : M →+ P) => AddMonoidHom.comp (AddEquiv.toAddMonoidHom g) (AddMonoidHom.comp h (AddEquiv.toAddMonoidHom (AddEquiv.symm f))), invFun := fun (k : N →+ Q) => AddMonoidHom.comp (AddEquiv.toAddMonoidHom (AddEquiv.symm g)) (AddMonoidHom.comp k (AddEquiv.toAddMonoidHom f)), left_inv := ⋯, right_inv := ⋯ }.toFun h + { toFun := fun (h : M →+ P) => AddMonoidHom.comp (AddEquiv.toAddMonoidHom g) (AddMonoidHom.comp h (AddEquiv.toAddMonoidHom (AddEquiv.symm f))), invFun := fun (k : N →+ Q) => AddMonoidHom.comp (AddEquiv.toAddMonoidHom (AddEquiv.symm g)) (AddMonoidHom.comp k (AddEquiv.toAddMonoidHom f)), left_inv := ⋯, right_inv := ⋯ }.toFun k

theorem AddEquiv.addMonoidHomCongr.proof_1 {M : Type u_2} {N : Type u_4} {P : Type u_1} {Q : Type u_3} [AddZeroClass M] [AddZeroClass N] [AddCommMonoid P] [AddCommMonoid Q] (f : M ≃+ N) (g : P ≃+ Q) (h : M →+ P) : (fun (k : N →+ Q) => AddMonoidHom.comp (AddEquiv.toAddMonoidHom (AddEquiv.symm g)) (AddMonoidHom.comp k (AddEquiv.toAddMonoidHom f))) ((fun (h : M →+ P) => AddMonoidHom.comp (AddEquiv.toAddMonoidHom g) (AddMonoidHom.comp h (AddEquiv.toAddMonoidHom (AddEquiv.symm f)))) h) = h

@[simp]

theorem AddEquiv.addMonoidHomCongr_apply {M : Type u_12} {N : Type u_13} {P : Type u_14} {Q : Type u_15} [AddZeroClass M] [AddZeroClass N] [AddCommMonoid P] [AddCommMonoid Q] (f : M ≃+ N) (g : P ≃+ Q) (h : M →+ P) : (AddEquiv.addMonoidHomCongr f g) h = AddMonoidHom.comp (AddEquiv.toAddMonoidHom g) (AddMonoidHom.comp h (AddEquiv.toAddMonoidHom (AddEquiv.symm f)))

@[simp]

theorem MulEquiv.monoidHomCongr_apply {M : Type u_12} {N : Type u_13} {P : Type u_14} {Q : Type u_15} [MulOneClass M] [MulOneClass N] [CommMonoid P] [CommMonoid Q] (f : M ≃* N) (g : P ≃* Q) (h : M →* P) : (MulEquiv.monoidHomCongr f g) h = MonoidHom.comp (MulEquiv.toMonoidHom g) (MonoidHom.comp h (MulEquiv.toMonoidHom (MulEquiv.symm f)))

def MulEquiv.monoidHomCongr {M : Type u_12} {N : Type u_13} {P : Type u_14} {Q : Type u_15} [MulOneClass M] [MulOneClass N] [CommMonoid P] [CommMonoid Q] (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.

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.

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

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) : { 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 := ⋯, right_inv := ⋯ }.toFun (x + y) = { 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 := ⋯, right_inv := ⋯ }.toFun x + { 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 := ⋯, right_inv := ⋯ }.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 : η) : (AddEquiv.piCongrRight es) 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 : η) : (MulEquiv.piCongrRight es) 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.

@[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) : AddEquiv.symm (AddEquiv.piCongrRight es) = AddEquiv.piCongrRight fun (i : η) => AddEquiv.symm (es i)

@[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.symm (MulEquiv.piCongrRight es) = 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.trans (AddEquiv.piCongrRight es) (AddEquiv.piCongrRight fs) = 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.trans (MulEquiv.piCongrRight es) (MulEquiv.piCongrRight fs) = MulEquiv.piCongrRight fun (i : η) => MulEquiv.trans (es i) (fs i)

theorem AddEquiv.piUnique.proof_1 {ι : Type u_2} (M : ι → Type u_1) [(j : ι) → Add (M j)] [Unique ι] : ∀ (x x_1 : (j : ι) → M j), (x + x_1) default = x default + x_1 default

def AddEquiv.piUnique {ι : Type u_12} (M : ι → Type u_13) [(j : ι) → Add (M j)] [Unique ι] : ((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

• AddEquiv.piUnique M = let __src := Equiv.piUnique M; { toEquiv := __src, map_add' := ⋯ }

@[simp]

theorem MulEquiv.piUnique_symm_apply {ι : Type u_12} (M : ι → Type u_13) [(j : ι) → Mul (M j)] [Unique ι] (x : M default) (i : ι) : (MulEquiv.symm (MulEquiv.piUnique M)) x i = uniqueElim x i

@[simp]

theorem MulEquiv.piUnique_apply {ι : Type u_12} (M : ι → Type u_13) [(j : ι) → Mul (M j)] [Unique ι] (f : (i : ι) → M i) : (MulEquiv.piUnique M) f = f default

@[simp]

theorem AddEquiv.piUnique_symm_apply {ι : Type u_12} (M : ι → Type u_13) [(j : ι) → Add (M j)] [Unique ι] (x : M default) (i : ι) : (AddEquiv.symm (AddEquiv.piUnique M)) x i = uniqueElim x i

@[simp]

theorem AddEquiv.piUnique_apply {ι : Type u_12} (M : ι → Type u_13) [(j : ι) → Add (M j)] [Unique ι] (f : (i : ι) → M i) : (AddEquiv.piUnique M) f = f default

def MulEquiv.piUnique {ι : Type u_12} (M : ι → Type u_13) [(j : ι) → Mul (M j)] [Unique ι] : ((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

• MulEquiv.piUnique M = let __src := Equiv.piUnique M; { toEquiv := __src, map_mul' := ⋯ }

Groups

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

An additive equivalence of additive groups preserves negation.

theorem MulEquiv.map_inv {G : Type u_10} {H : Type u_11} [Group G] [DivisionMonoid H] (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} [AddGroup G] [SubtractionMonoid H] (h : G ≃+ H) (x : G) (y : G) : h (x - y) = h x - h y

An additive equivalence of additive groups preserves subtractions.

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

A multiplicative equivalence of groups preserves division.

theorem AddHom.toAddEquiv.proof_2 {M : Type u_2} {N : Type u_1} [Add M] [Add N] (f : AddHom M N) (g : AddHom N M) (h₂ : AddHom.comp f g = AddHom.id N) (x : N) : (AddHom.comp f g) x = (AddHom.id N) x

theorem AddHom.toAddEquiv.proof_1 {M : Type u_1} {N : Type u_2} [Add M] [Add N] (f : AddHom M N) (g : AddHom N M) (h₁ : AddHom.comp g f = AddHom.id M) (x : M) : (AddHom.comp g f) x = (AddHom.id M) x

def AddHom.toAddEquiv {M : Type u_6} {N : Type u_7} [Add M] [Add N] (f : AddHom M N) (g : AddHom N M) (h₁ : AddHom.comp g f = AddHom.id M) (h₂ : AddHom.comp f g = AddHom.id N) : 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

• AddHom.toAddEquiv f g h₁ h₂ = { toEquiv := { toFun := ⇑f, invFun := ⇑g, left_inv := ⋯, right_inv := ⋯ }, map_add' := ⋯ }

def MulHom.toMulEquiv {M : Type u_6} {N : Type u_7} [Mul M] [Mul N] (f : M →ₙ* N) (g : N →ₙ* M) (h₁ : MulHom.comp g f = MulHom.id M) (h₂ : MulHom.comp f g = MulHom.id N) : 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

• MulHom.toMulEquiv f g h₁ h₂ = { toEquiv := { toFun := ⇑f, invFun := ⇑g, left_inv := ⋯, right_inv := ⋯ }, map_mul' := ⋯ }

@[simp]

theorem AddHom.toAddEquiv_apply {M : Type u_6} {N : Type u_7} [Add M] [Add N] (f : AddHom M N) (g : AddHom N M) (h₁ : AddHom.comp g f = AddHom.id M) (h₂ : AddHom.comp f g = AddHom.id N) : ⇑(AddHom.toAddEquiv f g h₁ h₂) = ⇑f

@[simp]

theorem MulHom.toMulEquiv_apply {M : Type u_6} {N : Type u_7} [Mul M] [Mul N] (f : M →ₙ* N) (g : N →ₙ* M) (h₁ : MulHom.comp g f = MulHom.id M) (h₂ : MulHom.comp f g = MulHom.id N) : ⇑(MulHom.toMulEquiv f g h₁ h₂) = ⇑f

@[simp]

theorem AddHom.toAddEquiv_symm_apply {M : Type u_6} {N : Type u_7} [Add M] [Add N] (f : AddHom M N) (g : AddHom N M) (h₁ : AddHom.comp g f = AddHom.id M) (h₂ : AddHom.comp f g = AddHom.id N) : ⇑(AddEquiv.symm (AddHom.toAddEquiv f g h₁ h₂)) = ⇑g

@[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₁ : MulHom.comp g f = MulHom.id M) (h₂ : MulHom.comp f g = MulHom.id N) : ⇑(MulEquiv.symm (MulHom.toMulEquiv f g h₁ h₂)) = ⇑g

theorem AddMonoidHom.toAddEquiv.proof_2 {M : Type u_2} {N : Type u_1} [AddZeroClass M] [AddZeroClass N] (f : M →+ N) (g : N →+ M) (h₂ : AddMonoidHom.comp f g = AddMonoidHom.id N) (x : N) : (AddMonoidHom.comp f g) x = (AddMonoidHom.id N) x

def AddMonoidHom.toAddEquiv {M : Type u_6} {N : Type u_7} [AddZeroClass M] [AddZeroClass N] (f : M →+ N) (g : N →+ M) (h₁ : AddMonoidHom.comp g f = AddMonoidHom.id M) (h₂ : AddMonoidHom.comp f g = AddMonoidHom.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 toFun = f and invFun = g. This constructor is useful if the underlying type(s) have specialized ext lemmas for additive monoid homomorphisms.

Equations

• AddMonoidHom.toAddEquiv f g h₁ h₂ = { toEquiv := { toFun := ⇑f, invFun := ⇑g, left_inv := ⋯, right_inv := ⋯ }, map_add' := ⋯ }

theorem AddMonoidHom.toAddEquiv.proof_1 {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (f : M →+ N) (g : N →+ M) (h₁ : AddMonoidHom.comp g f = AddMonoidHom.id M) (x : M) : (AddMonoidHom.comp g f) x = (AddMonoidHom.id M) x

@[simp]

theorem MonoidHom.toMulEquiv_symm_apply {M : Type u_6} {N : Type u_7} [MulOneClass M] [MulOneClass N] (f : M →* N) (g : N →* M) (h₁ : MonoidHom.comp g f = MonoidHom.id M) (h₂ : MonoidHom.comp f g = MonoidHom.id N) : ⇑(MulEquiv.symm (MonoidHom.toMulEquiv f g h₁ h₂)) = ⇑g

@[simp]

theorem AddMonoidHom.toAddEquiv_symm_apply {M : Type u_6} {N : Type u_7} [AddZeroClass M] [AddZeroClass N] (f : M →+ N) (g : N →+ M) (h₁ : AddMonoidHom.comp g f = AddMonoidHom.id M) (h₂ : AddMonoidHom.comp f g = AddMonoidHom.id N) : ⇑(AddEquiv.symm (AddMonoidHom.toAddEquiv f g h₁ h₂)) = ⇑g

@[simp]

theorem AddMonoidHom.toAddEquiv_apply {M : Type u_6} {N : Type u_7} [AddZeroClass M] [AddZeroClass N] (f : M →+ N) (g : N →+ M) (h₁ : AddMonoidHom.comp g f = AddMonoidHom.id M) (h₂ : AddMonoidHom.comp f g = AddMonoidHom.id N) : ⇑(AddMonoidHom.toAddEquiv f g h₁ h₂) = ⇑f

@[simp]

theorem MonoidHom.toMulEquiv_apply {M : Type u_6} {N : Type u_7} [MulOneClass M] [MulOneClass N] (f : M →* N) (g : N →* M) (h₁ : MonoidHom.comp g f = MonoidHom.id M) (h₂ : MonoidHom.comp f g = MonoidHom.id N) : ⇑(MonoidHom.toMulEquiv f g h₁ h₂) = ⇑f

def MonoidHom.toMulEquiv {M : Type u_6} {N : Type u_7} [MulOneClass M] [MulOneClass N] (f : M →* N) (g : N →* M) (h₁ : MonoidHom.comp g f = MonoidHom.id M) (h₂ : MonoidHom.comp f g = MonoidHom.id N) : 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

• MonoidHom.toMulEquiv f g h₁ h₂ = { toEquiv := { toFun := ⇑f, invFun := ⇑g, left_inv := ⋯, right_inv := ⋯ }, map_mul' := ⋯ }

def Equiv.neg (G : Type u_10) [InvolutiveNeg G] : Equiv.Perm G

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

Equations

• Equiv.neg G = Function.Involutive.toPerm Neg.neg ⋯

@[simp]

theorem Equiv.inv_apply (G : Type u_10) [InvolutiveInv G] : ⇑(Equiv.inv G) = Inv.inv

@[simp]

theorem Equiv.neg_apply (G : Type u_10) [InvolutiveNeg G] : ⇑(Equiv.neg G) = Neg.neg

def Equiv.inv (G : Type u_10) [InvolutiveInv G] : Equiv.Perm G

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

Equations

• Equiv.inv G = Function.Involutive.toPerm Inv.inv ⋯

@[simp]

theorem Equiv.neg_symm {G : Type u_10} [InvolutiveNeg G] : (Equiv.neg G).symm = Equiv.neg G

@[simp]

theorem Equiv.inv_symm {G : Type u_10} [InvolutiveInv G] : (Equiv.inv G).symm = Equiv.inv G