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

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

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

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

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

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

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

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

Instances For

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

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

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

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

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

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

Instances For

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Instances For

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

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

Instances For

source

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

(postcompEquiv e γ).symm g = e.symm.toAddMonoidHom.comp g

source

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

(postcompEquiv e γ).symm g = e.symm.toMonoidHom.comp g

source

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

(postcompEquiv e γ) f = e.toMonoidHom.comp f

source

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

(postcompEquiv e γ) f = e.toAddMonoidHom.comp f

source

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

Perm G

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

Equations

Instances For

source

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

Perm G

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

Equations

Instances For

source

@[simp]

theorem Equiv.neg_apply (G : Type u_14) [InvolutiveNeg G] :

⇑(Equiv.neg G) = Neg.neg

source

@[simp]

theorem Equiv.inv_apply (G : Type u_14) [InvolutiveInv G] :

⇑(Equiv.inv G) = Inv.inv

source

@[simp]

theorem Equiv.inv_symm {G : Type u_14} [InvolutiveInv G] :

Equiv.symm (Equiv.inv G) = Equiv.inv G

source

@[simp]

theorem Equiv.neg_symm {G : Type u_14} [InvolutiveNeg G] :

Equiv.symm (Equiv.neg G) = Equiv.neg G

Documentation

Mathlib.Algebra.Group.Equiv.Basic

Multiplicative and additive equivs #

Tags #

Monoids #