Transfer algebraic structures across Equivs

This continues the pattern set in Mathlib/Algebra/Group/TransferInstance.lean.

@[reducible, inline]

abbrev Equiv.mulAction (M : Type u_1) {α : Type u_4} {β : Type u_5} [Monoid M] (e : α ≃ β) [MulAction M β] : MulAction M α

Transfer MulAction across an Equiv

Equations

• Equiv.mulAction M e = { toSMul := Equiv.smul M e, mul_smul := ⋯, one_smul := ⋯ }

@[reducible, inline]

abbrev Equiv.addAction (M : Type u_1) {α : Type u_4} {β : Type u_5} [AddMonoid M] (e : α ≃ β) [AddAction M β] : AddAction M α

Transfer AddAction across an Equiv

Equations

• Equiv.addAction M e = { toVAdd := Equiv.vadd M e, add_vadd := ⋯, zero_vadd := ⋯ }

theorem Equiv.smulCommClass (M : Type u_1) (N : Type u_2) {α : Type u_4} {β : Type u_5} [SMul M β] [SMul N β] (e : α ≃ β) [SMulCommClass M N β] : SMulCommClass M N α

Transfer SMulCommClass across an Equiv

theorem Equiv.vaddCommClass (M : Type u_1) (N : Type u_2) {α : Type u_4} {β : Type u_5} [VAdd M β] [VAdd N β] (e : α ≃ β) [VAddCommClass M N β] : VAddCommClass M N α

Transfer VAddCommClass across an Equiv

theorem Equiv.isScalarTower (M : Type u_1) (N : Type u_2) {α : Type u_4} {β : Type u_5} [SMul M N] [SMul M β] [SMul N β] (e : α ≃ β) [IsScalarTower M N β] : IsScalarTower M N α

Transfer IsScalarTower across an Equiv

theorem Equiv.vaddAssocClass (M : Type u_1) (N : Type u_2) {α : Type u_4} {β : Type u_5} [VAdd M N] [VAdd M β] [VAdd N β] (e : α ≃ β) [VAddAssocClass M N β] : VAddAssocClass M N α

Transfer VAddAssocClass across an Equiv

theorem Equiv.isCentralScalar (M : Type u_1) {α : Type u_4} {β : Type u_5} [SMul M β] [SMul Mᵐᵒᵖ β] (e : α ≃ β) [IsCentralScalar M β] : IsCentralScalar M α

Transfer IsCentralScalar across an Equiv

theorem Equiv.isCentralVAdd (M : Type u_1) {α : Type u_4} {β : Type u_5} [VAdd M β] [VAdd Mᵃᵒᵖ β] (e : α ≃ β) [IsCentralVAdd M β] : IsCentralVAdd M α

Transfer IsCentralVAdd across an Equiv

@[reducible, inline]

abbrev Equiv.mulDistribMulAction (M : Type u_1) {N : Type u_2} {O : Type u_3} [Monoid M] [Monoid O] (e : N ≃ O) [MulDistribMulAction M O] : MulDistribMulAction M N

Transfer MulDistribMulAction across an Equiv

Equations

• Equiv.mulDistribMulAction M e = { toMulAction := Equiv.mulAction M e, smul_one := ⋯, smul_mul := ⋯ }

theorem Equiv.faithfulSMul (M : Type u_1) {α : Type u_4} {β : Type u_5} [SMul M β] (e : α ≃ β) [FaithfulSMul M β] : FaithfulSMul M α

Transfer FaithfulSMul across an Equiv.

See FaithfulSMul.of_injective for the general statement not about transferring.

theorem Equiv.faithfulVAdd (M : Type u_1) {α : Type u_4} {β : Type u_5} [VAdd M β] (e : α ≃ β) [FaithfulVAdd M β] : FaithfulVAdd M α

Transfer FaithfulVAdd across an Equiv

See FaithfulVAdd.of_injective for the general statement not about transferring.