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

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.

Equations

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

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' := ⋯ }

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 := ⋯ }

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 := ⋯ }

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.

Equations

• MulEquiv.funUnique α M = { toEquiv := Equiv.funUnique α M, map_mul' := ⋯ }

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.

Equations

• AddEquiv.funUnique α M = { toEquiv := Equiv.funUnique α M, map_add' := ⋯ }

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

@[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 AddEquiv.funUnique_symm_apply (α : Type u_2) (M : Type u_4) [Add 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.

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' := ⋯ }

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' := ⋯ }

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

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 := ⋯ }

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 := ⋯ }

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

Equations

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

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 := ⋯ }

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

Equations

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

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' := ⋯ }

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

Equations

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

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' := ⋯ }

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

Equations

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

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.

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

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

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' := ⋯ }

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' := ⋯ }

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

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

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

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

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

• Equiv.inv G = Function.Involutive.toPerm Inv.inv ⋯

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

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

Equations

• Equiv.neg G = Function.Involutive.toPerm Neg.neg ⋯

@[simp]

theorem Equiv.neg_apply (G : Type u_14) [InvolutiveNeg G] : ⇑(Equiv.neg G) = Neg.neg

@[simp]

theorem Equiv.inv_apply (G : Type u_14) [InvolutiveInv G] : ⇑(Equiv.inv G) = Inv.inv

@[simp]

theorem Equiv.inv_symm {G : Type u_14} [InvolutiveInv G] : Equiv.symm (Equiv.inv G) = Equiv.inv G

@[simp]

theorem Equiv.neg_symm {G : Type u_14} [InvolutiveNeg G] : Equiv.symm (Equiv.neg G) = Equiv.neg G