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.

Main definitions

• ≃* (MulEquiv), ≃+ (AddEquiv): bundled equivalences that preserve multiplication/addition (and are therefore monoid and group isomorphisms).
• MulEquivClass, AddEquivClass: classes for types containing bundled equivalences that preserve multiplication/addition.

Notation

• 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

@[simp]

theorem EmbeddingLike.map_eq_one_iff {F : Type u_1} {M : Type u_4} {N : Type u_5} [One M] [One N] [FunLike F M N] [EmbeddingLike F M N] [OneHomClass F M N] {f : F} {x : M} : f x = 1 ↔ x = 1

@[simp]

theorem EmbeddingLike.map_eq_zero_iff {F : Type u_1} {M : Type u_4} {N : Type u_5} [Zero M] [Zero N] [FunLike F M N] [EmbeddingLike F M N] [ZeroHomClass F M N] {f : F} {x : M} : f x = 0 ↔ x = 0

theorem EmbeddingLike.map_ne_one_iff {F : Type u_1} {M : Type u_4} {N : Type u_5} [One M] [One N] [FunLike F M N] [EmbeddingLike F M N] [OneHomClass F M N] {f : F} {x : M} : f x ≠ 1 ↔ x ≠ 1

theorem EmbeddingLike.map_ne_zero_iff {F : Type u_1} {M : Type u_4} {N : Type u_5} [Zero M] [Zero N] [FunLike F M N] [EmbeddingLike F M N] [ZeroHomClass F M N] {f : F} {x : M} : f x ≠ 0 ↔ x ≠ 0

structure AddEquiv (A : Type u_9) (B : Type u_10) [Add A] [Add B] extends A ≃ B, A →ₙ+ B : Type (max u_10 u_9)

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

class AddEquivClass (F : Type u_9) (A : outParam (Type u_10)) (B : outParam (Type u_11)) [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.

structure MulEquiv (M : Type u_9) (N : Type u_10) [Mul M] [Mul N] extends M ≃ N, M →ₙ* N : Type (max u_10 u_9)

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

def «term_≃*_» : Lean.TrailingParserDescr

Notation for a MulEquiv.

def «term_≃+_» : Lean.TrailingParserDescr

Notation for an AddEquiv.

theorem MulEquiv.toEquiv_injective {α : Type u_9} {β : Type u_10} [Mul α] [Mul β] : Function.Injective toEquiv

theorem AddEquiv.toEquiv_injective {α : Type u_9} {β : Type u_10} [Add α] [Add β] : Function.Injective toEquiv

class MulEquivClass (F : Type u_9) (A : outParam (Type u_10)) (B : outParam (Type u_11)) [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.

theorem MulEquivClass.map_eq_one_iff {F : Type u_1} {M : Type u_4} {N : Type u_5} [One M] [One N] [FunLike F M N] [EmbeddingLike F M N] [OneHomClass F M N] {f : F} {x : M} : f x = 1 ↔ x = 1

Alias of EmbeddingLike.map_eq_one_iff.

theorem AddEquivClass.map_eq_zero_iff {F : Type u_1} {M : Type u_4} {N : Type u_5} [Zero M] [Zero N] [FunLike F M N] [EmbeddingLike F M N] [ZeroHomClass F M N] {f : F} {x : M} : f x = 0 ↔ x = 0

theorem MulEquivClass.map_ne_one_iff {F : Type u_1} {M : Type u_4} {N : Type u_5} [One M] [One N] [FunLike F M N] [EmbeddingLike F M N] [OneHomClass F M N] {f : F} {x : M} : f x ≠ 1 ↔ x ≠ 1

Alias of EmbeddingLike.map_ne_one_iff.

theorem AddEquivClass.map_ne_zero_iff {F : Type u_1} {M : Type u_4} {N : Type u_5} [Zero M] [Zero N] [FunLike F M N] [EmbeddingLike F M N] [ZeroHomClass F M N] {f : F} {x : M} : f x ≠ 0 ↔ x ≠ 0

@[instance 100]

instance MulEquivClass.instMulHomClass {M : Type u_4} {N : Type u_5} (F : Type u_9) [Mul M] [Mul N] [EquivLike F M N] [h : MulEquivClass F M N] : MulHomClass F M N

@[instance 100]

instance AddEquivClass.instAddHomClass {M : Type u_4} {N : Type u_5} (F : Type u_9) [Add M] [Add N] [EquivLike F M N] [h : AddEquivClass F M N] : AddHomClass F M N

@[instance 100]

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

@[instance 100]

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

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 α ≃* β.

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 α ≃+ β.

instance instCoeTCMulEquivOfMulEquivClass {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.

instance instCoeTCAddEquivOfAddEquivClass {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.

instance MulEquiv.instEquivLike {M : Type u_4} {N : Type u_5} [Mul M] [Mul N] : EquivLike (M ≃* N) M N

instance AddEquiv.instEquivLike {M : Type u_4} {N : Type u_5} [Add M] [Add N] : EquivLike (M ≃+ N) M N

instance MulEquiv.instCoeFunForall {M : Type u_4} {N : Type u_5} [Mul M] [Mul N] : CoeFun (M ≃* N) fun (x : M ≃* N) => M → N

instance AddEquiv.instCoeFunForall {M : Type u_4} {N : Type u_5} [Add M] [Add N] : CoeFun (M ≃+ N) fun (x : M ≃+ N) => M → N

instance MulEquiv.instMulEquivClass {M : Type u_4} {N : Type u_5} [Mul M] [Mul N] : MulEquivClass (M ≃* N) M N

instance AddEquiv.instAddEquivClass {M : Type u_4} {N : Type u_5} [Add M] [Add N] : AddEquivClass (M ≃+ N) M N

theorem MulEquiv.ext {M : Type u_4} {N : Type u_5} [Mul M] [Mul N] {f g : M ≃* N} (h : ∀ (x : M), f x = g x) : f = g

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

theorem AddEquiv.ext {M : Type u_4} {N : Type u_5} [Add M] [Add N] {f g : M ≃+ N} (h : ∀ (x : M), f x = g x) : f = g

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

theorem MulEquiv.ext_iff {M : Type u_4} {N : Type u_5} [Mul M] [Mul N] {f g : M ≃* N} : f = g ↔ ∀ (x : M), f x = g x

theorem AddEquiv.ext_iff {M : Type u_4} {N : Type u_5} [Add M] [Add N] {f g : M ≃+ N} : f = g ↔ ∀ (x : M), f x = g x

theorem MulEquiv.congr_arg {M : Type u_4} {N : Type u_5} [Mul M] [Mul N] {f : M ≃* N} {x x' : M} : x = x' → f x = f x'

theorem AddEquiv.congr_arg {M : Type u_4} {N : Type u_5} [Add M] [Add N] {f : M ≃+ N} {x x' : M} : x = x' → f x = f x'

theorem MulEquiv.congr_fun {M : Type u_4} {N : Type u_5} [Mul M] [Mul N] {f g : M ≃* N} (h : f = g) (x : M) : f x = g x

theorem AddEquiv.congr_fun {M : Type u_4} {N : Type u_5} [Add M] [Add N] {f g : M ≃+ N} (h : f = g) (x : M) : f x = g x

@[simp]

theorem MulEquiv.coe_mk {M : Type u_4} {N : Type u_5} [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.coe_mk {M : Type u_4} {N : Type u_5} [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.mk_coe {M : Type u_4} {N : Type u_5} [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) : { toFun := ⇑e, invFun := e', left_inv := h₁, right_inv := h₂, map_mul' := h₃ } = e

@[simp]

theorem AddEquiv.mk_coe {M : Type u_4} {N : Type u_5} [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) : { toFun := ⇑e, invFun := e', left_inv := h₁, right_inv := h₂, map_add' := h₃ } = e

@[simp]

theorem MulEquiv.toEquiv_eq_coe {M : Type u_4} {N : Type u_5} [Mul M] [Mul N] (f : M ≃* N) : f.toEquiv = ↑f

@[simp]

theorem AddEquiv.toEquiv_eq_coe {M : Type u_4} {N : Type u_5} [Add M] [Add N] (f : M ≃+ N) : f.toEquiv = ↑f

@[simp]

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

The simp-normal form to turn something into a MulHom is via MulHomClass.toMulHom.

@[simp]

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

theorem MulEquiv.toFun_eq_coe {M : Type u_4} {N : Type u_5} [Mul M] [Mul N] (f : M ≃* N) : f.toFun = ⇑f

theorem AddEquiv.toFun_eq_coe {M : Type u_4} {N : Type u_5} [Add M] [Add N] (f : M ≃+ N) : f.toFun = ⇑f

@[simp]

theorem MulEquiv.coe_toEquiv {M : Type u_4} {N : Type u_5} [Mul M] [Mul N] (f : M ≃* N) : ⇑↑f = ⇑f

simp-normal form of toFun_eq_coe.

@[simp]

theorem AddEquiv.coe_toEquiv {M : Type u_4} {N : Type u_5} [Add M] [Add N] (f : M ≃+ N) : ⇑↑f = ⇑f

@[simp]

theorem MulEquiv.coe_toMulHom {M : Type u_4} {N : Type u_5} [Mul M] [Mul N] {f : M ≃* N} : ⇑f.toMulHom = ⇑f

@[simp]

theorem AddEquiv.coe_toAddHom {M : Type u_4} {N : Type u_5} [Add M] [Add N] {f : M ≃+ N} : ⇑f.toAddHom = ⇑f

def MulEquiv.mk' {M : Type u_4} {N : Type u_5} [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.

def AddEquiv.mk' {M : Type u_4} {N : Type u_5} [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.

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

A multiplicative isomorphism preserves multiplication.

theorem AddEquiv.map_add {M : Type u_4} {N : Type u_5} [Add M] [Add N] (f : M ≃+ N) (x y : M) : f (x + y) = f x + f y

An additive isomorphism preserves addition.

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

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

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

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

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

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

theorem MulEquiv.apply_eq_iff_eq {M : Type u_4} {N : Type u_5} [Mul M] [Mul N] (e : M ≃* N) {x y : M} : e x = e y ↔ x = y

theorem AddEquiv.apply_eq_iff_eq {M : Type u_4} {N : Type u_5} [Add M] [Add N] (e : M ≃+ N) {x y : M} : e x = e y ↔ x = y

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

The identity map is a multiplicative isomorphism.

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

The identity map is an additive isomorphism.

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

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

@[simp]

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

@[simp]

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

@[simp]

theorem MulEquiv.refl_apply {M : Type u_4} [Mul M] (m : M) : (refl M) m = m

@[simp]

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

theorem MulEquiv.symm_map_mul {M : Type u_9} {N : Type u_10} [Mul M] [Mul N] (h : M ≃* N) (x 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

theorem AddEquiv.symm_map_add {M : Type u_9} {N : Type u_10} [Add M] [Add N] (h : M ≃+ N) (x y : N) : h.symm (x + y) = h.symm x + h.symm y

def MulEquiv.symm {M : Type u_9} {N : Type u_10} [Mul M] [Mul N] (h : M ≃* N) : N ≃* M

The inverse of an isomorphism is an isomorphism.

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

The inverse of an isomorphism is an isomorphism.

theorem MulEquiv.invFun_eq_symm {M : Type u_4} {N : Type u_5} [Mul M] [Mul N] {f : M ≃* N} : f.invFun = ⇑f.symm

theorem AddEquiv.invFun_eq_symm {M : Type u_4} {N : Type u_5} [Add M] [Add N] {f : M ≃+ N} : f.invFun = ⇑f.symm

@[simp]

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

simp-normal form of invFun_eq_symm.

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem MulEquiv.toEquiv_symm {M : Type u_4} {N : Type u_5} [Mul M] [Mul N] (f : M ≃* N) : ↑f.symm = (↑f).symm

@[simp]

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

@[simp]

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

@[simp]

theorem AddEquiv.symm_symm {M : Type u_4} {N : Type u_5} [Add M] [Add N] (f : M ≃+ N) : f.symm.symm = f

theorem MulEquiv.symm_bijective {M : Type u_4} {N : Type u_5} [Mul M] [Mul N] : Function.Bijective symm

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

@[simp]

theorem MulEquiv.mk_coe' {M : Type u_4} {N : Type u_5} [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) : { toFun := f, invFun := ⇑e, left_inv := h₁, right_inv := h₂, map_mul' := h₃ } = e.symm

@[simp]

theorem AddEquiv.mk_coe' {M : Type u_4} {N : Type u_5} [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) : { toFun := f, invFun := ⇑e, left_inv := h₁, right_inv := h₂, map_add' := h₃ } = e.symm

@[simp]

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

@[simp]

theorem AddEquiv.symm_mk {M : Type u_4} {N : Type u_5} [Add M] [Add N] (f : M ≃ N) (h : ∀ (x y : M), f.toFun (x + y) = f.toFun x + f.toFun y) : { toEquiv := f, map_add' := h }.symm = { toEquiv := f.symm, map_add' := ⋯ }

@[simp]

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

@[simp]

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

@[simp]

theorem MulEquiv.apply_symm_apply {M : Type u_4} {N : Type u_5} [Mul M] [Mul N] (e : M ≃* N) (y : N) : e (e.symm y) = y

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

@[simp]

theorem AddEquiv.apply_symm_apply {M : Type u_4} {N : Type u_5} [Add M] [Add N] (e : M ≃+ N) (y : N) : e (e.symm y) = y

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

@[simp]

theorem MulEquiv.symm_apply_apply {M : Type u_4} {N : Type u_5} [Mul M] [Mul N] (e : M ≃* N) (x : M) : e.symm (e x) = x

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

@[simp]

theorem AddEquiv.symm_apply_apply {M : Type u_4} {N : Type u_5} [Add M] [Add N] (e : M ≃+ N) (x : M) : e.symm (e x) = x

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

@[simp]

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

@[simp]

theorem AddEquiv.symm_comp_self {M : Type u_4} {N : Type u_5} [Add M] [Add N] (e : M ≃+ N) : ⇑e.symm ∘ ⇑e = id

@[simp]

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

@[simp]

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

theorem MulEquiv.apply_eq_iff_symm_apply {M : Type u_4} {N : Type u_5} [Mul M] [Mul N] (e : M ≃* N) {x : M} {y : N} : e x = y ↔ x = e.symm y

theorem AddEquiv.apply_eq_iff_symm_apply {M : Type u_4} {N : Type u_5} [Add M] [Add N] (e : M ≃+ N) {x : M} {y : N} : e x = y ↔ x = e.symm y

theorem MulEquiv.symm_apply_eq {M : Type u_4} {N : Type u_5} [Mul M] [Mul N] (e : M ≃* N) {x : N} {y : M} : e.symm x = y ↔ x = e y

theorem AddEquiv.symm_apply_eq {M : Type u_4} {N : Type u_5} [Add M] [Add N] (e : M ≃+ N) {x : N} {y : M} : e.symm x = y ↔ x = e y

theorem MulEquiv.eq_symm_apply {M : Type u_4} {N : Type u_5} [Mul M] [Mul N] (e : M ≃* N) {x : N} {y : M} : y = e.symm x ↔ e y = x

theorem AddEquiv.eq_symm_apply {M : Type u_4} {N : Type u_5} [Add M] [Add N] (e : M ≃+ N) {x : N} {y : M} : y = e.symm x ↔ e y = x

theorem MulEquiv.eq_comp_symm {M : Type u_4} {N : Type u_5} [Mul M] [Mul N] {α : Type u_9} (e : M ≃* N) (f : N → α) (g : M → α) : f = g ∘ ⇑e.symm ↔ f ∘ ⇑e = g

theorem AddEquiv.eq_comp_symm {M : Type u_4} {N : Type u_5} [Add M] [Add N] {α : Type u_9} (e : M ≃+ N) (f : N → α) (g : M → α) : f = g ∘ ⇑e.symm ↔ f ∘ ⇑e = g

theorem MulEquiv.comp_symm_eq {M : Type u_4} {N : Type u_5} [Mul M] [Mul N] {α : Type u_9} (e : M ≃* N) (f : N → α) (g : M → α) : g ∘ ⇑e.symm = f ↔ g = f ∘ ⇑e

theorem AddEquiv.comp_symm_eq {M : Type u_4} {N : Type u_5} [Add M] [Add N] {α : Type u_9} (e : M ≃+ N) (f : N → α) (g : M → α) : g ∘ ⇑e.symm = f ↔ g = f ∘ ⇑e

theorem MulEquiv.eq_symm_comp {M : Type u_4} {N : Type u_5} [Mul M] [Mul N] {α : Type u_9} (e : M ≃* N) (f : α → M) (g : α → N) : f = ⇑e.symm ∘ g ↔ ⇑e ∘ f = g

theorem AddEquiv.eq_symm_comp {M : Type u_4} {N : Type u_5} [Add M] [Add N] {α : Type u_9} (e : M ≃+ N) (f : α → M) (g : α → N) : f = ⇑e.symm ∘ g ↔ ⇑e ∘ f = g

theorem MulEquiv.symm_comp_eq {M : Type u_4} {N : Type u_5} [Mul M] [Mul N] {α : Type u_9} (e : M ≃* N) (f : α → M) (g : α → N) : ⇑e.symm ∘ g = f ↔ g = ⇑e ∘ f

theorem AddEquiv.symm_comp_eq {M : Type u_4} {N : Type u_5} [Add M] [Add N] {α : Type u_9} (e : M ≃+ N) (f : α → M) (g : α → N) : ⇑e.symm ∘ g = f ↔ g = ⇑e ∘ f

@[simp]

theorem MulEquivClass.apply_coe_symm_apply {α : Type u_9} {β : Type u_10} [Mul α] [Mul β] {F : Type u_11} [EquivLike F α β] [MulEquivClass F α β] (e : F) (x : β) : e ((↑e).symm x) = x

@[simp]

theorem AddEquivClass.apply_coe_symm_apply {α : Type u_9} {β : Type u_10} [Add α] [Add β] {F : Type u_11} [EquivLike F α β] [AddEquivClass F α β] (e : F) (x : β) : e ((↑e).symm x) = x

@[simp]

theorem MulEquivClass.coe_symm_apply_apply {α : Type u_9} {β : Type u_10} [Mul α] [Mul β] {F : Type u_11} [EquivLike F α β] [MulEquivClass F α β] (e : F) (x : α) : (↑e).symm (e x) = x

@[simp]

theorem AddEquivClass.coe_symm_apply_apply {α : Type u_9} {β : Type u_10} [Add α] [Add β] {F : Type u_11} [EquivLike F α β] [AddEquivClass F α β] (e : F) (x : α) : (↑e).symm (e x) = x

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

See Note [custom simps projection]

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

See Note [custom simps projection]

def MulEquiv.trans {M : Type u_4} {N : Type u_5} {P : Type u_6} [Mul M] [Mul N] [Mul P] (h1 : M ≃* N) (h2 : N ≃* P) : M ≃* P

Transitivity of multiplication-preserving isomorphisms

def AddEquiv.trans {M : Type u_4} {N : Type u_5} {P : Type u_6} [Add M] [Add N] [Add P] (h1 : M ≃+ N) (h2 : N ≃+ P) : M ≃+ P

Transitivity of addition-preserving isomorphisms

@[simp]

theorem MulEquiv.coe_trans {M : Type u_4} {N : Type u_5} {P : Type u_6} [Mul M] [Mul N] [Mul P] (e₁ : M ≃* N) (e₂ : N ≃* P) : ⇑(e₁.trans e₂) = ⇑e₂ ∘ ⇑e₁

@[simp]

theorem AddEquiv.coe_trans {M : Type u_4} {N : Type u_5} {P : Type u_6} [Add M] [Add N] [Add P] (e₁ : M ≃+ N) (e₂ : N ≃+ P) : ⇑(e₁.trans e₂) = ⇑e₂ ∘ ⇑e₁

@[simp]

theorem MulEquiv.trans_apply {M : Type u_4} {N : Type u_5} {P : Type u_6} [Mul M] [Mul N] [Mul P] (e₁ : M ≃* N) (e₂ : N ≃* P) (m : M) : (e₁.trans e₂) m = e₂ (e₁ m)

@[simp]

theorem AddEquiv.trans_apply {M : Type u_4} {N : Type u_5} {P : Type u_6} [Add M] [Add N] [Add P] (e₁ : M ≃+ N) (e₂ : N ≃+ P) (m : M) : (e₁.trans e₂) m = e₂ (e₁ m)

@[simp]

theorem MulEquiv.symm_trans_apply {M : Type u_4} {N : Type u_5} {P : Type u_6} [Mul M] [Mul N] [Mul P] (e₁ : M ≃* N) (e₂ : N ≃* P) (p : P) : (e₁.trans e₂).symm p = e₁.symm (e₂.symm p)

@[simp]

theorem AddEquiv.symm_trans_apply {M : Type u_4} {N : Type u_5} {P : Type u_6} [Add M] [Add N] [Add P] (e₁ : M ≃+ N) (e₂ : N ≃+ P) (p : P) : (e₁.trans e₂).symm p = e₁.symm (e₂.symm p)

@[simp]

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

@[simp]

theorem AddEquiv.symm_trans_self {M : Type u_4} {N : Type u_5} [Add M] [Add N] (e : M ≃+ N) : e.symm.trans e = refl N

@[simp]

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

@[simp]

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

def MulEquiv.symmEquiv (P : Type u_9) (Q : Type u_10) [Mul P] [Mul Q] : P ≃* Q ≃ (Q ≃* P)

MulEquiv.symm defines an equivalence between α ≃* β and β ≃* α.

def AddEquiv.symmEquiv (P : Type u_9) (Q : Type u_10) [Add P] [Add Q] : P ≃+ Q ≃ (Q ≃+ P)

AddEquiv.symm defines an equivalence between α ≃+ β and β ≃+ α

@[simp]

theorem MulEquiv.symmEquiv_apply_apply (P : Type u_9) (Q : Type u_10) [Mul P] [Mul Q] (h : P ≃* Q) (a✝ : Q) : ((symmEquiv P Q) h) a✝ = h.symm a✝

@[simp]

theorem MulEquiv.symmEquiv_symm_apply_symm_apply (P : Type u_9) (Q : Type u_10) [Mul P] [Mul Q] (h : Q ≃* P) (a✝ : Q) : ((symmEquiv P Q).symm h).symm a✝ = h a✝

@[simp]

theorem AddEquiv.symmEquiv_symm_apply_symm_apply (P : Type u_9) (Q : Type u_10) [Add P] [Add Q] (h : Q ≃+ P) (a✝ : Q) : ((symmEquiv P Q).symm h).symm a✝ = h a✝

@[simp]

theorem AddEquiv.symmEquiv_apply_apply (P : Type u_9) (Q : Type u_10) [Add P] [Add Q] (h : P ≃+ Q) (a✝ : Q) : ((symmEquiv P Q) h) a✝ = h.symm a✝

@[simp]

theorem MulEquiv.symmEquiv_symm_apply_apply (P : Type u_9) (Q : Type u_10) [Mul P] [Mul Q] (h : Q ≃* P) (a✝ : P) : ((symmEquiv P Q).symm h) a✝ = h.symm a✝

@[simp]

theorem AddEquiv.symmEquiv_apply_symm_apply (P : Type u_9) (Q : Type u_10) [Add P] [Add Q] (h : P ≃+ Q) (a✝ : P) : ((symmEquiv P Q) h).symm a✝ = h a✝

@[simp]

theorem AddEquiv.symmEquiv_symm_apply_apply (P : Type u_9) (Q : Type u_10) [Add P] [Add Q] (h : Q ≃+ P) (a✝ : P) : ((symmEquiv P Q).symm h) a✝ = h.symm a✝

@[simp]

theorem MulEquiv.symmEquiv_apply_symm_apply (P : Type u_9) (Q : Type u_10) [Mul P] [Mul Q] (h : P ≃* Q) (a✝ : P) : ((symmEquiv P Q) h).symm a✝ = h a✝

def MulEquiv.cast {ι : Type u_9} {M : ι → Type u_10} [(i : ι) → Mul (M i)] {i j : ι} (h : i = j) : M i ≃* M j

Equiv.cast (congrArg _ h) as a MulEquiv.

Note that unlike Equiv.cast, this takes an equality of indices rather than an equality of types, to avoid having to deal with an equality of the algebraic structure itself.

def AddEquiv.cast {ι : Type u_9} {M : ι → Type u_10} [(i : ι) → Add (M i)] {i j : ι} (h : i = j) : M i ≃+ M j

Equiv.cast (congrArg _ h) as an AddEquiv.

Note that unlike Equiv.cast, this takes an equality of indices rather than an equality of types, to avoid having to deal with an equality of the algebraic structure itself.

@[simp]

theorem AddEquiv.cast_symm_apply {ι : Type u_9} {M : ι → Type u_10} [(i : ι) → Add (M i)] {i j : ι} (h : i = j) (a : M j) : (AddEquiv.cast h).symm a = cast ⋯ a

@[simp]

theorem AddEquiv.cast_apply {ι : Type u_9} {M : ι → Type u_10} [(i : ι) → Add (M i)] {i j : ι} (h : i = j) (a : M i) : (AddEquiv.cast h) a = cast ⋯ a

@[simp]

theorem MulEquiv.cast_apply {ι : Type u_9} {M : ι → Type u_10} [(i : ι) → Mul (M i)] {i j : ι} (h : i = j) (a : M i) : (MulEquiv.cast h) a = cast ⋯ a

@[simp]

theorem MulEquiv.cast_symm_apply {ι : Type u_9} {M : ι → Type u_10} [(i : ι) → Mul (M i)] {i j : ι} (h : i = j) (a : M j) : (MulEquiv.cast h).symm a = cast ⋯ a

Monoids

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

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

theorem MulEquiv.map_one {M : Type u_4} {N : Type u_5} [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_zero {M : Type u_4} {N : Type u_5} [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_eq_one_iff {M : Type u_4} {N : Type u_5} [MulOneClass M] [MulOneClass N] (h : M ≃* N) {x : M} : h x = 1 ↔ x = 1

theorem AddEquiv.map_eq_zero_iff {M : Type u_4} {N : Type u_5} [AddZeroClass M] [AddZeroClass N] (h : M ≃+ N) {x : M} : h x = 0 ↔ x = 0

theorem MulEquiv.map_ne_one_iff {M : Type u_4} {N : Type u_5} [MulOneClass M] [MulOneClass N] (h : M ≃* N) {x : M} : h x ≠ 1 ↔ x ≠ 1

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

noncomputable def MulEquiv.ofBijective {M : Type u_9} {N : Type u_10} {F : Type u_11} [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

noncomputable def AddEquiv.ofBijective {M : Type u_9} {N : Type u_10} {F : Type u_11} [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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

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

@[simp]

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

@[simp]

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

@[simp]

theorem MulEquiv.toMonoidHom_eq_coe {M : Type u_4} {N : Type u_5} [MulOneClass M] [MulOneClass N] (f : M ≃* N) : f.toMonoidHom = ↑f

@[simp]

theorem AddEquiv.toAddMonoidHom_eq_coe {M : Type u_4} {N : Type u_5} [AddZeroClass M] [AddZeroClass N] (f : M ≃+ N) : f.toAddMonoidHom = ↑f

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

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

Groups

theorem MulEquiv.map_inv {G : Type u_7} {H : Type u_8} [Group G] [DivisionMonoid H] (h : G ≃* H) (x : G) : h x⁻¹ = (h x)⁻¹

A multiplicative equivalence of groups preserves inversion.

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

An additive equivalence of additive groups preserves negation.

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

A multiplicative equivalence of groups preserves division.

theorem AddEquiv.map_sub {G : Type u_7} {H : Type u_8} [AddGroup G] [SubtractionMonoid H] (h : G ≃+ H) (x y : G) : h (x - y) = h x - h y

An additive equivalence of additive groups preserves subtractions.

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

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

@[simp]

theorem AddHom.toAddEquiv_apply {M : Type u_4} {N : Type u_5} [Add M] [Add N] (f : M →ₙ+ N) (g : N →ₙ+ M) (h₁ : g.comp f = id M) (h₂ : f.comp g = id N) : ⇑(f.toAddEquiv g h₁ h₂) = ⇑f

@[simp]

theorem AddHom.toAddEquiv_symm_apply {M : Type u_4} {N : Type u_5} [Add M] [Add N] (f : M →ₙ+ N) (g : N →ₙ+ M) (h₁ : g.comp f = id M) (h₂ : f.comp g = id N) : ⇑(f.toAddEquiv g h₁ h₂).symm = ⇑g

@[simp]

theorem MulHom.toMulEquiv_symm_apply {M : Type u_4} {N : Type u_5} [Mul M] [Mul N] (f : M →ₙ* N) (g : N →ₙ* M) (h₁ : g.comp f = id M) (h₂ : f.comp g = id N) : ⇑(f.toMulEquiv g h₁ h₂).symm = ⇑g

@[simp]

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

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

def AddMonoidHom.toAddEquiv {M : Type u_4} {N : Type u_5} [AddZeroClass M] [AddZeroClass N] (f : M →+ N) (g : N →+ M) (h₁ : g.comp f = id M) (h₂ : f.comp g = 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.

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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