Documentation

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

Function.Injective toAddEquiv

theorem MulEquivClass.isDedekindFiniteMonoid_iff {F : Type u_1} {α : Type u_2} {β : Type u_3} [EquivLike F α β] [MulOne α] [MulOne β] [MulEquivClass F α β] [OneHomClass F α β] (f : F) :

IsDedekindFiniteMonoid α ↔ IsDedekindFiniteMonoid β

theorem AddEquivClass.isDedekindFiniteAddMonoid_iff {F : Type u_1} {α : Type u_2} {β : Type u_3} [EquivLike F α β] [AddZero α] [AddZero β] [AddEquivClass F α β] [ZeroHomClass F α β] (f : F) :

IsDedekindFiniteAddMonoid α ↔ IsDedekindFiniteAddMonoid β

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.

Instances For

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.

Instances For

@[implicit_reducible]

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.

@[implicit_reducible]

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.

def MulEquiv.funUnique (α : Type u_2) (M : Type u_4) [Mul M] [Unique α] :

(α → M) ≃* M

If α has a unique term, then the product of magmas α → M is isomorphic to M.

Instances For

def AddEquiv.funUnique (α : Type u_2) (M : Type u_4) [Add M] [Unique α] :

(α → M) ≃+ M

If α has a unique term, then the product of magmas α → M is isomorphic to M.

Instances For

@[simp]

theorem AddEquiv.funUnique_symm_apply (α : Type u_2) (M : Type u_4) [Add M] [Unique α] (x : M) (i : α) :

(funUnique α M).symm x i = x

@[simp]

theorem MulEquiv.funUnique_apply (α : Type u_2) (M : Type u_4) [Mul M] [Unique α] (f : (i : α) → (fun (a : α) => M) i) :

(funUnique α M) f = f default

@[simp]

theorem AddEquiv.funUnique_apply (α : Type u_2) (M : Type u_4) [Add M] [Unique α] (f : (i : α) → (fun (a : α) => M) i) :

(funUnique α M) f = f default

@[simp]

theorem MulEquiv.funUnique_symm_apply (α : Type u_2) (M : Type u_4) [Mul M] [Unique α] (x : M) (i : α) :

(funUnique α M).symm x i = x

Monoids #

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.

Instances For

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.

Instances For

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

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

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

Instances For

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

Instances For

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

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

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

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

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

Instances For

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

Instances For

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

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

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

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

@[simp]

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

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

@[simp]

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

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

@[simp]

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

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

@[simp]

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

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

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

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

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

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

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

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

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

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

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

Instances For

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

Instances For

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

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

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

Instances For

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

Instances For

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

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

@[simp]

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

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

@[simp]

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

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

@[simp]

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

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

@[simp]

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

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

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

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

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

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

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

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

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

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

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.

Instances For

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.

Instances For

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

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

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

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

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

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

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