Sigma instances for additive and multiplicative actions #
This file defines instances for arbitrary sum of additive and multiplicative actions.
See also #
def
Sigma.instIsScalarTowerSigmaInstVAddSigmaInstVAddSigma.proof_1
{ι : Type u_1}
{M : Type u_2}
{N : Type u_3}
{α : ι → Type u_4}
[inst : (i : ι) → VAdd M (α i)]
[inst : (i : ι) → VAdd N (α i)]
[inst : VAdd M N]
[inst : ∀ (i : ι), VAddAssocClass M N (α i)]
:
VAddAssocClass M N ((i : ι) × α i)
Equations
- (_ : VAddAssocClass M N ((i : ι) × α i)) = (_ : VAddAssocClass M N ((i : ι) × α i))
instance
Sigma.instIsScalarTowerSigmaInstVAddSigmaInstVAddSigma
{ι : Type u_1}
{M : Type u_2}
{N : Type u_3}
{α : ι → Type u_4}
[inst : (i : ι) → VAdd M (α i)]
[inst : (i : ι) → VAdd N (α i)]
[inst : VAdd M N]
[inst : ∀ (i : ι), VAddAssocClass M N (α i)]
:
VAddAssocClass M N ((i : ι) × α i)
instance
Sigma.instIsScalarTowerSigmaInstSMulSigmaInstSMulSigma
{ι : Type u_1}
{M : Type u_2}
{N : Type u_3}
{α : ι → Type u_4}
[inst : (i : ι) → SMul M (α i)]
[inst : (i : ι) → SMul N (α i)]
[inst : SMul M N]
[inst : ∀ (i : ι), IsScalarTower M N (α i)]
:
IsScalarTower M N ((i : ι) × α i)
instance
Sigma.instVAddCommClassSigmaInstVAddSigmaInstVAddSigma
{ι : Type u_1}
{M : Type u_2}
{N : Type u_3}
{α : ι → Type u_4}
[inst : (i : ι) → VAdd M (α i)]
[inst : (i : ι) → VAdd N (α i)]
[inst : ∀ (i : ι), VAddCommClass M N (α i)]
:
VAddCommClass M N ((i : ι) × α i)
def
Sigma.instVAddCommClassSigmaInstVAddSigmaInstVAddSigma.proof_1
{ι : Type u_1}
{M : Type u_2}
{N : Type u_3}
{α : ι → Type u_4}
[inst : (i : ι) → VAdd M (α i)]
[inst : (i : ι) → VAdd N (α i)]
[inst : ∀ (i : ι), VAddCommClass M N (α i)]
:
VAddCommClass M N ((i : ι) × α i)
Equations
- (_ : VAddCommClass M N ((i : ι) × α i)) = (_ : VAddCommClass M N ((i : ι) × α i))
instance
Sigma.instSMulCommClassSigmaInstSMulSigmaInstSMulSigma
{ι : Type u_1}
{M : Type u_2}
{N : Type u_3}
{α : ι → Type u_4}
[inst : (i : ι) → SMul M (α i)]
[inst : (i : ι) → SMul N (α i)]
[inst : ∀ (i : ι), SMulCommClass M N (α i)]
:
SMulCommClass M N ((i : ι) × α i)
def
Sigma.instIsCentralVAddSigmaInstVAddSigmaAddOpposite.proof_1
{ι : Type u_1}
{M : Type u_2}
{α : ι → Type u_3}
[inst : (i : ι) → VAdd M (α i)]
[inst : (i : ι) → VAdd Mᵃᵒᵖ (α i)]
[inst : ∀ (i : ι), IsCentralVAdd M (α i)]
:
IsCentralVAdd M ((i : ι) × α i)
Equations
- (_ : IsCentralVAdd M ((i : ι) × α i)) = (_ : IsCentralVAdd M ((i : ι) × α i))
instance
Sigma.instIsCentralVAddSigmaInstVAddSigmaAddOpposite
{ι : Type u_1}
{M : Type u_2}
{α : ι → Type u_3}
[inst : (i : ι) → VAdd M (α i)]
[inst : (i : ι) → VAdd Mᵃᵒᵖ (α i)]
[inst : ∀ (i : ι), IsCentralVAdd M (α i)]
:
IsCentralVAdd M ((i : ι) × α i)
instance
Sigma.instIsCentralScalarSigmaInstSMulSigmaMulOpposite
{ι : Type u_1}
{M : Type u_2}
{α : ι → Type u_3}
[inst : (i : ι) → SMul M (α i)]
[inst : (i : ι) → SMul Mᵐᵒᵖ (α i)]
[inst : ∀ (i : ι), IsCentralScalar M (α i)]
:
IsCentralScalar M ((i : ι) × α i)
theorem
Sigma.FaithfulVAdd'
{ι : Type u_3}
{M : Type u_1}
{α : ι → Type u_2}
[inst : (i : ι) → VAdd M (α i)]
(i : ι)
[inst : FaithfulVAdd M (α i)]
:
FaithfulVAdd M ((i : ι) × α i)
This is not an instance because i
becomes a metavariable.
theorem
Sigma.FaithfulSMul'
{ι : Type u_3}
{M : Type u_1}
{α : ι → Type u_2}
[inst : (i : ι) → SMul M (α i)]
(i : ι)
[inst : FaithfulSMul M (α i)]
:
FaithfulSMul M ((i : ι) × α i)
This is not an instance because i
becomes a metavariable.
instance
Sigma.instFaithfulVAddSigmaInstVAddSigma
{ι : Type u_1}
{M : Type u_2}
{α : ι → Type u_3}
[inst : (i : ι) → VAdd M (α i)]
[inst : Nonempty ι]
[inst : ∀ (i : ι), FaithfulVAdd M (α i)]
:
FaithfulVAdd M ((i : ι) × α i)
def
Sigma.instFaithfulVAddSigmaInstVAddSigma.proof_1
{ι : Type u_1}
{M : Type u_2}
{α : ι → Type u_3}
[inst : (i : ι) → VAdd M (α i)]
[inst : Nonempty ι]
[inst : ∀ (i : ι), FaithfulVAdd M (α i)]
:
FaithfulVAdd M ((i : ι) × α i)
Equations
- (_ : FaithfulVAdd M ((i : ι) × α i)) = (_ : FaithfulVAdd M ((i : ι) × α i))
instance
Sigma.instFaithfulSMulSigmaInstSMulSigma
{ι : Type u_1}
{M : Type u_2}
{α : ι → Type u_3}
[inst : (i : ι) → SMul M (α i)]
[inst : Nonempty ι]
[inst : ∀ (i : ι), FaithfulSMul M (α i)]
:
FaithfulSMul M ((i : ι) × α i)