Transfer algebraic structures across Equivs #
This continues the pattern set in Mathlib/Algebra/Group/TransferInstance.lean.
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]
:
Transfer MulDistribMulAction across an Equiv
Equations
- Equiv.mulDistribMulAction M e = { toMulAction := Equiv.mulAction M e, smul_mul := ⋯, smul_one := ⋯ }