Multiplicative and additive equivs #

This file contains basic results on MulEquiv and AddEquiv.

Tags #

Equiv, MulEquiv, AddEquiv

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

Function.Injective toMulEquiv

source

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

Function.Injective toAddEquiv

source

def MulEquiv.ofUnique {M : Type u_16} {N : Type u_17} [Unique M] [Unique N] [Mul M] [Mul N] :

M ≃* N

The MulEquiv between two monoids with a unique element.

Equations

MulEquiv.ofUnique = { toEquiv := Equiv.ofUnique M N, map_mul' := ⋯ }

Instances For

source

def AddEquiv.ofUnique {M : Type u_16} {N : Type u_17} [Unique M] [Unique N] [Add M] [Add N] :

M ≃+ N

The AddEquiv between two AddMonoids with a unique element.

Equations

AddEquiv.ofUnique = { toEquiv := Equiv.ofUnique M N, map_add' := ⋯ }

Instances For

source

instance MulEquiv.instUnique {M : Type u_16} {N : Type u_17} [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.instUnique = { default := MulEquiv.ofUnique, uniq := ⋯ }

source

instance AddEquiv.instUnique {M : Type u_16} {N : Type u_17} [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.instUnique = { default := AddEquiv.ofUnique, uniq := ⋯ }

Monoids #

source

def MulEquiv.arrowCongr {M : Type u_16} {N : Type u_17} {P : Type u_18} {Q : Type u_19} [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

MulEquiv.arrowCongr f g = { toFun := fun (h : M → P) (n : N) => g (h (f.symm n)), invFun := fun (k : N → Q) (m : M) => g.symm (k (f m)), left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ }

Instances For

source

def AddEquiv.arrowCongr {M : Type u_16} {N : Type u_17} {P : Type u_18} {Q : Type u_19} [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

AddEquiv.arrowCongr f g = { toFun := fun (h : M → P) (n : N) => g (h (f.symm n)), invFun := fun (k : N → Q) (m : M) => g.symm (k (f m)), left_inv := ⋯, right_inv := ⋯, map_add' := ⋯ }

Instances For

source

@[simp]

theorem AddEquiv.arrowCongr_apply {M : Type u_16} {N : Type u_17} {P : Type u_18} {Q : Type u_19} [Add P] [Add Q] (f : M ≃ N) (g : P ≃+ Q) (h : M → P) (n : N) :

(arrowCongr f g) h n = g (h (f.symm n))

source

@[simp]

theorem MulEquiv.arrowCongr_apply {M : Type u_16} {N : Type u_17} {P : Type u_18} {Q : Type u_19} [Mul P] [Mul Q] (f : M ≃ N) (g : P ≃* Q) (h : M → P) (n : N) :

(arrowCongr f g) h n = g (h (f.symm n))

source

def MulEquiv.monoidHomCongrLeftEquiv {M₁ : Type u_5} {M₂ : Type u_6} {N : Type u_8} [MulOneClass M₁] [MulOneClass M₂] [Monoid N] (e : M₁ ≃* M₂) :

(M₁ →* N) ≃ (M₂ →* N)

The equivalence (M₁ →* N) ≃ (M₂ →* N) obtained by postcomposition with a multiplicative equivalence e : M₁ ≃* M₂.

Equations

e.monoidHomCongrLeftEquiv = { toFun := fun (f : M₁ →* N) => f.comp e.symm.toMonoidHom, invFun := fun (f : M₂ →* N) => f.comp e.toMonoidHom, left_inv := ⋯, right_inv := ⋯ }

Instances For

source

def AddEquiv.addMonoidHomCongrLeftEquiv {M₁ : Type u_5} {M₂ : Type u_6} {N : Type u_8} [AddZeroClass M₁] [AddZeroClass M₂] [AddMonoid N] (e : M₁ ≃+ M₂) :

(M₁ →+ N) ≃ (M₂ →+ N)

The equivalence (M₁ →+ N) ≃ (M₂ →+ N) obtained by postcomposition with an additive equivalence e : M₁ ≃+ M₂.

Equations

e.addMonoidHomCongrLeftEquiv = { toFun := fun (f : M₁ →+ N) => f.comp e.symm.toAddMonoidHom, invFun := fun (f : M₂ →+ N) => f.comp e.toAddMonoidHom, left_inv := ⋯, right_inv := ⋯ }

Instances For

source

@[simp]

theorem AddEquiv.addMonoidHomCongrLeftEquiv_symm_apply {M₁ : Type u_5} {M₂ : Type u_6} {N : Type u_8} [AddZeroClass M₁] [AddZeroClass M₂] [AddMonoid N] (e : M₁ ≃+ M₂) (f : M₂ →+ N) :

e.addMonoidHomCongrLeftEquiv.symm f = f.comp e.toAddMonoidHom

source

@[simp]

theorem MulEquiv.monoidHomCongrLeftEquiv_symm_apply {M₁ : Type u_5} {M₂ : Type u_6} {N : Type u_8} [MulOneClass M₁] [MulOneClass M₂] [Monoid N] (e : M₁ ≃* M₂) (f : M₂ →* N) :

e.monoidHomCongrLeftEquiv.symm f = f.comp e.toMonoidHom

source

@[simp]

theorem AddEquiv.addMonoidHomCongrLeftEquiv_apply {M₁ : Type u_5} {M₂ : Type u_6} {N : Type u_8} [AddZeroClass M₁] [AddZeroClass M₂] [AddMonoid N] (e : M₁ ≃+ M₂) (f : M₁ →+ N) :

e.addMonoidHomCongrLeftEquiv f = f.comp e.symm.toAddMonoidHom

source

@[simp]

theorem MulEquiv.monoidHomCongrLeftEquiv_apply {M₁ : Type u_5} {M₂ : Type u_6} {N : Type u_8} [MulOneClass M₁] [MulOneClass M₂] [Monoid N] (e : M₁ ≃* M₂) (f : M₁ →* N) :

e.monoidHomCongrLeftEquiv f = f.comp e.symm.toMonoidHom

source

def MulEquiv.monoidHomCongrRightEquiv {M : Type u_4} {N₁ : Type u_9} {N₂ : Type u_10} [MulOneClass M] [Monoid N₁] [Monoid N₂] (e : N₁ ≃* N₂) :

(M →* N₁) ≃ (M →* N₂)

The equivalence (M →* N₁) ≃ (M →* N₂) obtained by postcomposition with a multiplicative equivalence e : N₁ ≃* N₂.

Equations

e.monoidHomCongrRightEquiv = { toFun := e.toMonoidHom.comp, invFun := e.symm.toMonoidHom.comp, left_inv := ⋯, right_inv := ⋯ }

Instances For

source

def AddEquiv.addMonoidHomCongrRightEquiv {M : Type u_4} {N₁ : Type u_9} {N₂ : Type u_10} [AddZeroClass M] [AddMonoid N₁] [AddMonoid N₂] (e : N₁ ≃+ N₂) :

(M →+ N₁) ≃ (M →+ N₂)

The equivalence (M →+ N₁) ≃ (M →+ N₂) obtained by postcomposition with an additive equivalence e : N₁ ≃+ N₂.

Equations

e.addMonoidHomCongrRightEquiv = { toFun := e.toAddMonoidHom.comp, invFun := e.symm.toAddMonoidHom.comp, left_inv := ⋯, right_inv := ⋯ }

Instances For

source

@[simp]

theorem MulEquiv.monoidHomCongrRightEquiv_apply {M : Type u_4} {N₁ : Type u_9} {N₂ : Type u_10} [MulOneClass M] [Monoid N₁] [Monoid N₂] (e : N₁ ≃* N₂) (hmn : M →* N₁) :

e.monoidHomCongrRightEquiv hmn = e.toMonoidHom.comp hmn

source

@[simp]

theorem MulEquiv.monoidHomCongrRightEquiv_symm_apply {M : Type u_4} {N₁ : Type u_9} {N₂ : Type u_10} [MulOneClass M] [Monoid N₁] [Monoid N₂] (e : N₁ ≃* N₂) (hmn : M →* N₂) :

e.monoidHomCongrRightEquiv.symm hmn = e.symm.toMonoidHom.comp hmn

source

@[simp]

theorem AddEquiv.addMonoidHomCongrRightEquiv_symm_apply {M : Type u_4} {N₁ : Type u_9} {N₂ : Type u_10} [AddZeroClass M] [AddMonoid N₁] [AddMonoid N₂] (e : N₁ ≃+ N₂) (hmn : M →+ N₂) :

e.addMonoidHomCongrRightEquiv.symm hmn = e.symm.toAddMonoidHom.comp hmn

source

@[simp]

theorem AddEquiv.addMonoidHomCongrRightEquiv_apply {M : Type u_4} {N₁ : Type u_9} {N₂ : Type u_10} [AddZeroClass M] [AddMonoid N₁] [AddMonoid N₂] (e : N₁ ≃+ N₂) (hmn : M →+ N₁) :

e.addMonoidHomCongrRightEquiv hmn = e.toAddMonoidHom.comp hmn

source

@[simp]

theorem MulEquiv.monoidHomCongrLeftEquiv_refl {M : Type u_4} {N : Type u_8} [MulOneClass M] [Monoid N] :

(refl M).monoidHomCongrLeftEquiv = Equiv.refl (M →* N)

source

@[simp]

theorem AddEquiv.addMonoidHomCongrLeftEquiv_refl {M : Type u_4} {N : Type u_8} [AddZeroClass M] [AddMonoid N] :

(refl M).addMonoidHomCongrLeftEquiv = Equiv.refl (M →+ N)

source

@[simp]

theorem MulEquiv.monoidHomCongrRightEquiv_refl {M : Type u_4} {N : Type u_8} [MulOneClass M] [Monoid N] :

(refl N).monoidHomCongrRightEquiv = Equiv.refl (M →* N)

source

@[simp]

theorem AddEquiv.addMonoidHomCongrRightEquiv_refl {M : Type u_4} {N : Type u_8} [AddZeroClass M] [AddMonoid N] :

(refl N).addMonoidHomCongrRightEquiv = Equiv.refl (M →+ N)

source

@[simp]

theorem MulEquiv.symm_monoidHomCongrLeftEquiv {M₁ : Type u_5} {M₂ : Type u_6} {N : Type u_8} [MulOneClass M₁] [MulOneClass M₂] [Monoid N] (e : M₁ ≃* M₂) :

e.monoidHomCongrLeftEquiv.symm = e.symm.monoidHomCongrLeftEquiv

source

@[simp]

theorem AddEquiv.symm_addMonoidHomCongrLeftEquiv {M₁ : Type u_5} {M₂ : Type u_6} {N : Type u_8} [AddZeroClass M₁] [AddZeroClass M₂] [AddMonoid N] (e : M₁ ≃+ M₂) :

e.addMonoidHomCongrLeftEquiv.symm = e.symm.addMonoidHomCongrLeftEquiv

source

@[simp]

theorem MulEquiv.symm_monoidHomCongrRightEquiv {M : Type u_4} {N₁ : Type u_9} {N₂ : Type u_10} [MulOneClass M] [Monoid N₁] [Monoid N₂] (e : N₁ ≃* N₂) :

e.monoidHomCongrRightEquiv.symm = e.symm.monoidHomCongrRightEquiv

source

@[simp]

theorem AddEquiv.symm_addMonoidHomCongrRightEquiv {M : Type u_4} {N₁ : Type u_9} {N₂ : Type u_10} [AddZeroClass M] [AddMonoid N₁] [AddMonoid N₂] (e : N₁ ≃+ N₂) :

e.addMonoidHomCongrRightEquiv.symm = e.symm.addMonoidHomCongrRightEquiv

source

@[simp]

theorem MulEquiv.monoidHomCongrLeftEquiv_trans {M₁ : Type u_5} {M₂ : Type u_6} {M₃ : Type u_7} {N : Type u_8} [MulOneClass M₁] [MulOneClass M₂] [MulOneClass M₃] [Monoid N] (e₁₂ : M₁ ≃* M₂) (e₂₃ : M₂ ≃* M₃) :

(e₁₂.trans e₂₃).monoidHomCongrLeftEquiv = e₁₂.monoidHomCongrLeftEquiv.trans e₂₃.monoidHomCongrLeftEquiv

source

@[simp]

theorem AddEquiv.addMonoidHomCongrLeftEquiv_trans {M₁ : Type u_5} {M₂ : Type u_6} {M₃ : Type u_7} {N : Type u_8} [AddZeroClass M₁] [AddZeroClass M₂] [AddZeroClass M₃] [AddMonoid N] (e₁₂ : M₁ ≃+ M₂) (e₂₃ : M₂ ≃+ M₃) :

(e₁₂.trans e₂₃).addMonoidHomCongrLeftEquiv = e₁₂.addMonoidHomCongrLeftEquiv.trans e₂₃.addMonoidHomCongrLeftEquiv

source

@[simp]

theorem MulEquiv.monoidHomCongrRightEquiv_trans {M : Type u_4} {N₁ : Type u_9} {N₂ : Type u_10} {N₃ : Type u_11} [MulOneClass M] [Monoid N₁] [Monoid N₂] [Monoid N₃] (e₁₂ : N₁ ≃* N₂) (e₂₃ : N₂ ≃* N₃) :

(e₁₂.trans e₂₃).monoidHomCongrRightEquiv = e₁₂.monoidHomCongrRightEquiv.trans e₂₃.monoidHomCongrRightEquiv

source

@[simp]

theorem AddEquiv.addMonoidHomCongrRightEquiv_trans {M : Type u_4} {N₁ : Type u_9} {N₂ : Type u_10} {N₃ : Type u_11} [AddZeroClass M] [AddMonoid N₁] [AddMonoid N₂] [AddMonoid N₃] (e₁₂ : N₁ ≃+ N₂) (e₂₃ : N₂ ≃+ N₃) :

(e₁₂.trans e₂₃).addMonoidHomCongrRightEquiv = e₁₂.addMonoidHomCongrRightEquiv.trans e₂₃.addMonoidHomCongrRightEquiv

source

def MulEquiv.monoidHomCongrLeft {M₁ : Type u_5} {M₂ : Type u_6} {N : Type u_8} [MulOneClass M₁] [MulOneClass M₂] [CommMonoid N] (e : M₁ ≃* M₂) :

(M₁ →* N) ≃* (M₂ →* N)

The isomorphism (M₁ →* N) ≃* (M₂ →* N) obtained by postcomposition with a multiplicative equivalence e : M₁ ≃* M₂.

Equations

e.monoidHomCongrLeft = { toEquiv := e.monoidHomCongrLeftEquiv, map_mul' := ⋯ }

Instances For

source

def AddEquiv.addMonoidHomCongrLeft {M₁ : Type u_5} {M₂ : Type u_6} {N : Type u_8} [AddZeroClass M₁] [AddZeroClass M₂] [AddCommMonoid N] (e : M₁ ≃+ M₂) :

(M₁ →+ N) ≃+ (M₂ →+ N)

The isomorphism (M₁ →+ N) ≃+ (M₂ →+ N) obtained by postcomposition with an additive equivalence e : M₁ ≃+ M₂.

Equations

e.addMonoidHomCongrLeft = { toEquiv := e.addMonoidHomCongrLeftEquiv, map_add' := ⋯ }

Instances For

source

@[simp]

theorem MulEquiv.monoidHomCongrLeft_apply {M₁ : Type u_5} {M₂ : Type u_6} {N : Type u_8} [MulOneClass M₁] [MulOneClass M₂] [CommMonoid N] (e : M₁ ≃* M₂) (f : M₁ →* N) :

e.monoidHomCongrLeft f = f.comp ↑e.symm

source

@[simp]

theorem AddEquiv.addMonoidHomCongrLeft_apply {M₁ : Type u_5} {M₂ : Type u_6} {N : Type u_8} [AddZeroClass M₁] [AddZeroClass M₂] [AddCommMonoid N] (e : M₁ ≃+ M₂) (f : M₁ →+ N) :

e.addMonoidHomCongrLeft f = f.comp ↑e.symm

source

def MulEquiv.monoidHomCongrRight {M : Type u_4} {N₁ : Type u_9} {N₂ : Type u_10} [MulOneClass M] [CommMonoid N₁] [CommMonoid N₂] (e : N₁ ≃* N₂) :

(M →* N₁) ≃* (M →* N₂)

The isomorphism (M →* N₁) ≃* (M →* N₂) obtained by postcomposition with a multiplicative equivalence e : N₁ ≃* N₂.

Equations

e.monoidHomCongrRight = { toEquiv := e.monoidHomCongrRightEquiv, map_mul' := ⋯ }

Instances For

source

def AddEquiv.addMonoidHomCongrRight {M : Type u_4} {N₁ : Type u_9} {N₂ : Type u_10} [AddZeroClass M] [AddCommMonoid N₁] [AddCommMonoid N₂] (e : N₁ ≃+ N₂) :

(M →+ N₁) ≃+ (M →+ N₂)

The isomorphism (M →+ N₁) ≃+ (M →+ N₂) obtained by postcomposition with an additive equivalence e : N₁ ≃+ N₂.

Equations

e.addMonoidHomCongrRight = { toEquiv := e.addMonoidHomCongrRightEquiv, map_add' := ⋯ }

Instances For

source

@[simp]

theorem AddEquiv.addMonoidHomCongrRight_apply {M : Type u_4} {N₁ : Type u_9} {N₂ : Type u_10} [AddZeroClass M] [AddCommMonoid N₁] [AddCommMonoid N₂] (e : N₁ ≃+ N₂) (hmn : M →+ N₁) :

e.addMonoidHomCongrRight hmn = (↑e).comp hmn

source

@[simp]

theorem MulEquiv.monoidHomCongrRight_apply {M : Type u_4} {N₁ : Type u_9} {N₂ : Type u_10} [MulOneClass M] [CommMonoid N₁] [CommMonoid N₂] (e : N₁ ≃* N₂) (hmn : M →* N₁) :

e.monoidHomCongrRight hmn = (↑e).comp hmn

source

@[simp]

theorem MulEquiv.monoidHomCongrLeft_refl {M : Type u_4} {N : Type u_8} [MulOneClass M] [CommMonoid N] :

(refl M).monoidHomCongrLeft = refl (M →* N)

source

@[simp]

theorem AddEquiv.addMonoidHomCongrLeft_refl {M : Type u_4} {N : Type u_8} [AddZeroClass M] [AddCommMonoid N] :

(refl M).addMonoidHomCongrLeft = refl (M →+ N)

source

@[simp]

theorem MulEquiv.monoidHomCongrRight_refl {M : Type u_4} {N : Type u_8} [MulOneClass M] [CommMonoid N] :

(refl N).monoidHomCongrRight = refl (M →* N)

source

@[simp]

theorem AddEquiv.addMonoidHomCongrRight_refl {M : Type u_4} {N : Type u_8} [AddZeroClass M] [AddCommMonoid N] :

(refl N).addMonoidHomCongrRight = refl (M →+ N)

source

@[simp]

theorem MulEquiv.symm_monoidHomCongrLeft {M₁ : Type u_5} {M₂ : Type u_6} {N : Type u_8} [MulOneClass M₁] [MulOneClass M₂] [CommMonoid N] (e : M₁ ≃* M₂) :

e.monoidHomCongrLeft.symm = e.symm.monoidHomCongrLeft

source

@[simp]

theorem AddEquiv.symm_addMonoidHomCongrLeft {M₁ : Type u_5} {M₂ : Type u_6} {N : Type u_8} [AddZeroClass M₁] [AddZeroClass M₂] [AddCommMonoid N] (e : M₁ ≃+ M₂) :

e.addMonoidHomCongrLeft.symm = e.symm.addMonoidHomCongrLeft

source

@[simp]

theorem MulEquiv.symm_monoidHomCongrRight {M : Type u_4} {N₁ : Type u_9} {N₂ : Type u_10} [MulOneClass M] [CommMonoid N₁] [CommMonoid N₂] (e : N₁ ≃* N₂) :

e.monoidHomCongrRight.symm = e.symm.monoidHomCongrRight

source

@[simp]

theorem AddEquiv.symm_addMonoidHomCongrRight {M : Type u_4} {N₁ : Type u_9} {N₂ : Type u_10} [AddZeroClass M] [AddCommMonoid N₁] [AddCommMonoid N₂] (e : N₁ ≃+ N₂) :

e.addMonoidHomCongrRight.symm = e.symm.addMonoidHomCongrRight

source

@[simp]

theorem MulEquiv.monoidHomCongrLeft_trans {M₁ : Type u_5} {M₂ : Type u_6} {M₃ : Type u_7} {N : Type u_8} [MulOneClass M₁] [MulOneClass M₂] [MulOneClass M₃] [CommMonoid N] (e₁₂ : M₁ ≃* M₂) (e₂₃ : M₂ ≃* M₃) :

(e₁₂.trans e₂₃).monoidHomCongrLeft = e₁₂.monoidHomCongrLeft.trans e₂₃.monoidHomCongrLeft

source

@[simp]

theorem AddEquiv.addMonoidHomCongrLeft_trans {M₁ : Type u_5} {M₂ : Type u_6} {M₃ : Type u_7} {N : Type u_8} [AddZeroClass M₁] [AddZeroClass M₂] [AddZeroClass M₃] [AddCommMonoid N] (e₁₂ : M₁ ≃+ M₂) (e₂₃ : M₂ ≃+ M₃) :

(e₁₂.trans e₂₃).addMonoidHomCongrLeft = e₁₂.addMonoidHomCongrLeft.trans e₂₃.addMonoidHomCongrLeft

source

@[simp]

theorem MulEquiv.monoidHomCongrRight_trans {M : Type u_4} {N₁ : Type u_9} {N₂ : Type u_10} {N₃ : Type u_11} [MulOneClass M] [CommMonoid N₁] [CommMonoid N₂] [CommMonoid N₃] (e₁₂ : N₁ ≃* N₂) (e₂₃ : N₂ ≃* N₃) :

(e₁₂.trans e₂₃).monoidHomCongrRight = e₁₂.monoidHomCongrRight.trans e₂₃.monoidHomCongrRight

source

@[simp]

theorem AddEquiv.addMonoidHomCongrRight_trans {M : Type u_4} {N₁ : Type u_9} {N₂ : Type u_10} {N₃ : Type u_11} [AddZeroClass M] [AddCommMonoid N₁] [AddCommMonoid N₂] [AddCommMonoid N₃] (e₁₂ : N₁ ≃+ N₂) (e₂₃ : N₂ ≃+ N₃) :

(e₁₂.trans e₂₃).addMonoidHomCongrRight = e₁₂.addMonoidHomCongrRight.trans e₂₃.addMonoidHomCongrRight

source

@[deprecated MulEquiv.monoidHomCongrLeft (since := "2025-08-12")]

def MulEquiv.monoidHomCongr {M : Type u_16} {N : Type u_17} {P : Type u_18} {Q : Type u_19} [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

f.monoidHomCongr g = f.monoidHomCongrLeft.trans g.monoidHomCongrRight

Instances For

source

@[deprecated MulEquiv.monoidHomCongrLeft (since := "2025-08-12")]

def AddEquiv.addMonoidHomCongr {M : Type u_16} {N : Type u_17} {P : Type u_18} {Q : Type u_19} [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

f.addMonoidHomCongr g = f.addMonoidHomCongrLeft.trans g.addMonoidHomCongrRight

Instances For

source

def MulEquiv.piCongrRight {η : Type u_16} {Ms : η → Type u_17} {Ns : η → Type u_18} [(j : η) → Mul (Ms j)] [(j : η) → Mul (Ns j)] (es : (j : η) → Ms j ≃* Ns j) :

((j : η) → Ms j) ≃* ((j : η) → Ns j)

A family of multiplicative equivalences Π j, (Ms j ≃* Ns j) generates a multiplicative equivalence between Π j, Ms j and Π j, Ns j.

This is the MulEquiv version of Equiv.piCongrRight, and the dependent version of MulEquiv.arrowCongr.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

def AddEquiv.piCongrRight {η : Type u_16} {Ms : η → Type u_17} {Ns : η → Type u_18} [(j : η) → Add (Ms j)] [(j : η) → Add (Ns j)] (es : (j : η) → Ms j ≃+ Ns j) :

((j : η) → Ms j) ≃+ ((j : η) → Ns j)

A family of additive equivalences Π j, (Ms j ≃+ Ns j) generates an additive equivalence between Π j, Ms j and Π j, Ns j.

This is the AddEquiv version of Equiv.piCongrRight, and the dependent version of AddEquiv.arrowCongr.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

@[simp]

theorem AddEquiv.piCongrRight_apply {η : Type u_16} {Ms : η → Type u_17} {Ns : η → Type u_18} [(j : η) → Add (Ms j)] [(j : η) → Add (Ns j)] (es : (j : η) → Ms j ≃+ Ns j) (x : (j : η) → Ms j) (j : η) :

(piCongrRight es) x j = (es j) (x j)

source

@[simp]

theorem MulEquiv.piCongrRight_apply {η : Type u_16} {Ms : η → Type u_17} {Ns : η → Type u_18} [(j : η) → Mul (Ms j)] [(j : η) → Mul (Ns j)] (es : (j : η) → Ms j ≃* Ns j) (x : (j : η) → Ms j) (j : η) :

(piCongrRight es) x j = (es j) (x j)

source

@[simp]

theorem MulEquiv.piCongrRight_refl {η : Type u_16} {Ms : η → Type u_17} [(j : η) → Mul (Ms j)] :

(piCongrRight fun (j : η) => refl (Ms j)) = refl ((j : η) → Ms j)

source

@[simp]

theorem AddEquiv.piCongrRight_refl {η : Type u_16} {Ms : η → Type u_17} [(j : η) → Add (Ms j)] :

(piCongrRight fun (j : η) => refl (Ms j)) = refl ((j : η) → Ms j)

source

@[simp]

theorem MulEquiv.piCongrRight_symm {η : Type u_16} {Ms : η → Type u_17} {Ns : η → Type u_18} [(j : η) → Mul (Ms j)] [(j : η) → Mul (Ns j)] (es : (j : η) → Ms j ≃* Ns j) :

(piCongrRight es).symm = piCongrRight fun (i : η) => (es i).symm

source

@[simp]

theorem AddEquiv.piCongrRight_symm {η : Type u_16} {Ms : η → Type u_17} {Ns : η → Type u_18} [(j : η) → Add (Ms j)] [(j : η) → Add (Ns j)] (es : (j : η) → Ms j ≃+ Ns j) :

(piCongrRight es).symm = piCongrRight fun (i : η) => (es i).symm

source

@[simp]

theorem MulEquiv.piCongrRight_trans {η : Type u_16} {Ms : η → Type u_17} {Ns : η → Type u_18} {Ps : η → Type u_19} [(j : η) → Mul (Ms j)] [(j : η) → Mul (Ns j)] [(j : η) → Mul (Ps j)] (es : (j : η) → Ms j ≃* Ns j) (fs : (j : η) → Ns j ≃* Ps j) :

(piCongrRight es).trans (piCongrRight fs) = piCongrRight fun (i : η) => (es i).trans (fs i)

source

@[simp]

theorem AddEquiv.piCongrRight_trans {η : Type u_16} {Ms : η → Type u_17} {Ns : η → Type u_18} {Ps : η → Type u_19} [(j : η) → Add (Ms j)] [(j : η) → Add (Ns j)] [(j : η) → Add (Ps j)] (es : (j : η) → Ms j ≃+ Ns j) (fs : (j : η) → Ns j ≃+ Ps j) :

(piCongrRight es).trans (piCongrRight fs) = piCongrRight fun (i : η) => (es i).trans (fs i)

source

def MulEquiv.piUnique {ι : Type u_16} (M : ι → Type u_17) [(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 = { toEquiv := Equiv.piUnique M, map_mul' := ⋯ }

Instances For

source

def AddEquiv.piUnique {ι : Type u_16} (M : ι → Type u_17) [(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 = { toEquiv := Equiv.piUnique M, map_add' := ⋯ }

Instances For

source

@[simp]

theorem MulEquiv.piUnique_symm_apply {ι : Type u_16} (M : ι → Type u_17) [(j : ι) → Mul (M j)] [Unique ι] (x : M default) (i : ι) :

(piUnique M).symm x i = uniqueElim x i

source

@[simp]

theorem AddEquiv.piUnique_symm_apply {ι : Type u_16} (M : ι → Type u_17) [(j : ι) → Add (M j)] [Unique ι] (x : M default) (i : ι) :

(piUnique M).symm x i = uniqueElim x i

source

@[simp]

theorem MulEquiv.piUnique_apply {ι : Type u_16} (M : ι → Type u_17) [(j : ι) → Mul (M j)] [Unique ι] (f : (i : ι) → M i) :

(piUnique M) f = f default

source

@[simp]

theorem AddEquiv.piUnique_apply {ι : Type u_16} (M : ι → Type u_17) [(j : ι) → Add (M j)] [Unique ι] (f : (i : ι) → M i) :

(piUnique M) f = f default

source

@[deprecated MulEquiv.monoidHomCongrLeftEquiv (since := "2025-08-12")]

def MonoidHom.precompEquiv {α : Type u_19} {β : Type u_20} [Monoid α] [Monoid β] (e : α ≃* β) (γ : Type u_21) [Monoid γ] :

(β →* γ) ≃ (α →* γ)

The equivalence (β →* γ) ≃ (α →* γ) obtained by precomposition with a multiplicative equivalence e : α ≃* β.

Equations

MonoidHom.precompEquiv e γ = { toFun := fun (f : β →* γ) => f.comp ↑e, invFun := fun (g : α →* γ) => g.comp ↑e.symm, left_inv := ⋯, right_inv := ⋯ }

Instances For

source

@[deprecated MulEquiv.monoidHomCongrLeftEquiv (since := "2025-08-12")]

def AddMonoidHom.precompEquiv {α : Type u_19} {β : Type u_20} [AddMonoid α] [AddMonoid β] (e : α ≃+ β) (γ : Type u_21) [AddMonoid γ] :

(β →+ γ) ≃ (α →+ γ)

The equivalence (β →+ γ) ≃ (α →+ γ) obtained by precomposition with an additive equivalence e : α ≃+ β.

Equations

AddMonoidHom.precompEquiv e γ = { toFun := fun (f : β →+ γ) => f.comp ↑e, invFun := fun (g : α →+ γ) => g.comp ↑e.symm, left_inv := ⋯, right_inv := ⋯ }

Instances For

source

theorem AddMonoidHom.precompEquiv_apply {α : Type u_19} {β : Type u_20} [AddMonoid α] [AddMonoid β] (e : α ≃+ β) (γ : Type u_21) [AddMonoid γ] (f : β →+ γ) :

(precompEquiv e γ) f = f.comp ↑e

source

theorem MonoidHom.precompEquiv_symm_apply {α : Type u_19} {β : Type u_20} [Monoid α] [Monoid β] (e : α ≃* β) (γ : Type u_21) [Monoid γ] (g : α →* γ) :

(precompEquiv e γ).symm g = g.comp ↑e.symm

source

theorem MonoidHom.precompEquiv_apply {α : Type u_19} {β : Type u_20} [Monoid α] [Monoid β] (e : α ≃* β) (γ : Type u_21) [Monoid γ] (f : β →* γ) :

(precompEquiv e γ) f = f.comp ↑e

source

theorem AddMonoidHom.precompEquiv_symm_apply {α : Type u_19} {β : Type u_20} [AddMonoid α] [AddMonoid β] (e : α ≃+ β) (γ : Type u_21) [AddMonoid γ] (g : α →+ γ) :

(precompEquiv e γ).symm g = g.comp ↑e.symm

source

@[deprecated MulEquiv.monoidHomCongrRightEquiv (since := "2025-08-12")]

def MonoidHom.postcompEquiv {α : Type u_19} {β : Type u_20} [Monoid α] [Monoid β] (e : α ≃* β) (γ : Type u_21) [Monoid γ] :

(γ →* α) ≃ (γ →* β)

The equivalence (γ →* α) ≃ (γ →* β) obtained by postcomposition with a multiplicative equivalence e : α ≃* β.

Equations

MonoidHom.postcompEquiv e γ = { toFun := fun (f : γ →* α) => e.toMonoidHom.comp f, invFun := fun (g : γ →* β) => e.symm.toMonoidHom.comp g, left_inv := ⋯, right_inv := ⋯ }

Instances For

source

@[deprecated MulEquiv.monoidHomCongrRightEquiv (since := "2025-08-12")]

def AddMonoidHom.postcompEquiv {α : Type u_19} {β : Type u_20} [AddMonoid α] [AddMonoid β] (e : α ≃+ β) (γ : Type u_21) [AddMonoid γ] :

(γ →+ α) ≃ (γ →+ β)

The equivalence (γ →+ α) ≃ (γ →+ β) obtained by postcomposition with an additive equivalence e : α ≃+ β.

Equations

AddMonoidHom.postcompEquiv e γ = { toFun := fun (f : γ →+ α) => e.toAddMonoidHom.comp f, invFun := fun (g : γ →+ β) => e.symm.toAddMonoidHom.comp g, left_inv := ⋯, right_inv := ⋯ }