Sigma instances for additive and multiplicative actions #
This file defines instances for arbitrary sum of additive and multiplicative actions.
See also #
@[implicit_reducible]
instance
Sigma.instSMul_mathlib
{ι : Type u_1}
{M : Type u_2}
{α : ι → Type u_4}
[(i : ι) → SMul M (α i)]
:
SMul M ((i : ι) × α i)
@[implicit_reducible]
instance
Sigma.VAdd
{ι : Type u_1}
{M : Type u_2}
{α : ι → Type u_4}
[(i : ι) → _root_.VAdd M (α i)]
:
_root_.VAdd M ((i : ι) × α i)
theorem
Sigma.smul_def
{ι : Type u_1}
{M : Type u_2}
{α : ι → Type u_4}
[(i : ι) → SMul M (α i)]
(a : M)
(x : (i : ι) × α i)
:
a • x = map id (fun (x : ι) (x_1 : α x) => a • x_1) x
theorem
Sigma.vadd_def
{ι : Type u_1}
{M : Type u_2}
{α : ι → Type u_4}
[(i : ι) → _root_.VAdd M (α i)]
(a : M)
(x : (i : ι) × α i)
:
@[simp]
theorem
Sigma.smul_mk
{ι : Type u_1}
{M : Type u_2}
{α : ι → Type u_4}
[(i : ι) → SMul M (α i)]
(a : M)
(i : ι)
(b : α i)
:
a • ⟨i, b⟩ = ⟨i, a • b⟩
@[simp]
theorem
Sigma.vadd_mk
{ι : Type u_1}
{M : Type u_2}
{α : ι → Type u_4}
[(i : ι) → _root_.VAdd M (α i)]
(a : M)
(i : ι)
(b : α i)
:
instance
Sigma.instIsScalarTowerOfSMul
{ι : Type u_1}
{M : Type u_2}
{N : Type u_3}
{α : ι → Type u_4}
[(i : ι) → SMul M (α i)]
[(i : ι) → SMul N (α i)]
[SMul M N]
[∀ (i : ι), IsScalarTower M N (α i)]
:
IsScalarTower M N ((i : ι) × α i)
instance
Sigma.instVAddAssocClassOfVAdd
{ι : Type u_1}
{M : Type u_2}
{N : Type u_3}
{α : ι → Type u_4}
[(i : ι) → _root_.VAdd M (α i)]
[(i : ι) → _root_.VAdd N (α i)]
[_root_.VAdd M N]
[∀ (i : ι), VAddAssocClass M N (α i)]
:
VAddAssocClass M N ((i : ι) × α i)
instance
Sigma.instSMulCommClass
{ι : Type u_1}
{M : Type u_2}
{N : Type u_3}
{α : ι → Type u_4}
[(i : ι) → SMul M (α i)]
[(i : ι) → SMul N (α i)]
[∀ (i : ι), SMulCommClass M N (α i)]
:
SMulCommClass M N ((i : ι) × α i)
instance
Sigma.instVAddCommClass
{ι : Type u_1}
{M : Type u_2}
{N : Type u_3}
{α : ι → Type u_4}
[(i : ι) → _root_.VAdd M (α i)]
[(i : ι) → _root_.VAdd N (α i)]
[∀ (i : ι), VAddCommClass M N (α i)]
:
VAddCommClass M N ((i : ι) × α i)
instance
Sigma.instIsCentralScalar
{ι : Type u_1}
{M : Type u_2}
{α : ι → Type u_4}
[(i : ι) → SMul M (α i)]
[(i : ι) → SMul Mᵐᵒᵖ (α i)]
[∀ (i : ι), IsCentralScalar M (α i)]
:
IsCentralScalar M ((i : ι) × α i)
instance
Sigma.instIsCentralVAdd
{ι : Type u_1}
{M : Type u_2}
{α : ι → Type u_4}
[(i : ι) → _root_.VAdd M (α i)]
[(i : ι) → _root_.VAdd Mᵃᵒᵖ (α i)]
[∀ (i : ι), IsCentralVAdd M (α i)]
:
IsCentralVAdd M ((i : ι) × α i)
theorem
Sigma.FaithfulSMul'
{ι : Type u_1}
{M : Type u_2}
{α : ι → Type u_4}
[(i : ι) → SMul M (α i)]
(i : ι)
[FaithfulSMul M (α i)]
:
FaithfulSMul M ((i : ι) × α i)
This is not an instance because i becomes a metavariable.
theorem
Sigma.FaithfulVAdd'
{ι : Type u_1}
{M : Type u_2}
{α : ι → Type u_4}
[(i : ι) → _root_.VAdd M (α i)]
(i : ι)
[FaithfulVAdd M (α i)]
:
FaithfulVAdd M ((i : ι) × α i)
This is not an instance because i becomes a metavariable.
instance
Sigma.instFaithfulSMulOfNonempty
{ι : Type u_1}
{M : Type u_2}
{α : ι → Type u_4}
[(i : ι) → SMul M (α i)]
[Nonempty ι]
[∀ (i : ι), FaithfulSMul M (α i)]
:
FaithfulSMul M ((i : ι) × α i)
instance
Sigma.instFaithfulVAddOfNonempty
{ι : Type u_1}
{M : Type u_2}
{α : ι → Type u_4}
[(i : ι) → _root_.VAdd M (α i)]
[Nonempty ι]
[∀ (i : ι), FaithfulVAdd M (α i)]
:
FaithfulVAdd M ((i : ι) × α i)
@[implicit_reducible]
@[implicit_reducible]