Documentation

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

Instances For

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.

Instances

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

Instances For

def «term_≃*_» :

Lean.TrailingParserDescr

Notation for a MulEquiv.

Instances For

def «term_≃+_» :

Lean.TrailingParserDescr

Notation for an AddEquiv.

Instances For

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.

Instances

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

Instances For

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

Instances For

@[implicit_reducible]

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.

@[implicit_reducible]

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.

@[implicit_reducible]

instance MulEquiv.instEquivLike {M : Type u_4} {N : Type u_5} [Mul M] [Mul N] :

EquivLike (M ≃* N) M N

@[implicit_reducible]

instance AddEquiv.instEquivLike {M : Type u_4} {N : Type u_5} [Add M] [Add N] :

EquivLike (M ≃+ N) M N

@[implicit_reducible]

instance MulEquiv.instCoeFunForall {M : Type u_4} {N : Type u_5} [Mul M] [Mul N] :

CoeFun (M ≃* N) fun (x : M ≃* N) => M → N

@[implicit_reducible]

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.

Instances For

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.

Instances For

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.

Instances For

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

M ≃+ M

The identity map is an additive isomorphism.

Instances For

@[implicit_reducible]

instance MulEquiv.instInhabited {M : Type u_4} [Mul M] :

Inhabited (M ≃* M)

@[implicit_reducible]

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.

Instances For

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.

Instances For

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]

Instances For

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]

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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.

Instances For

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

Instances For

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

Instances For

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

Instances For

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.

Instances For

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

Instances For

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.

Instances For

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

Instances For

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.

Instances For