# mathlibdocumentation

group_theory.group_action.sigma

# Sigma instances for additive and multiplicative actions #

This file defines instances for arbitrary sum of additive and multiplicative actions.

• group_theory.group_action.pi
• group_theory.group_action.prod
• group_theory.group_action.sum
@[protected, instance]
def sigma.has_smul {ι : Type u_1} {M : Type u_2} {α : ι → Type u_4} [Π (i : ι), (α i)] :
(Σ (i : ι), α i)
Equations
@[protected, instance]
def sigma.has_vadd {ι : Type u_1} {M : Type u_2} {α : ι → Type u_4} [Π (i : ι), (α i)] :
(Σ (i : ι), α i)
Equations
theorem sigma.smul_def {ι : Type u_1} {M : Type u_2} {α : ι → Type u_4} [Π (i : ι), (α i)] (a : M) (x : Σ (i : ι), α i) :
a x = (λ (i : ι), x
theorem sigma.vadd_def {ι : Type u_1} {M : Type u_2} {α : ι → Type u_4} [Π (i : ι), (α i)] (a : M) (x : Σ (i : ι), α i) :
a +ᵥ x = (λ (i : ι), x
@[simp]
theorem sigma.vadd_mk {ι : Type u_1} {M : Type u_2} {α : ι → Type u_4} [Π (i : ι), (α i)] (a : M) (i : ι) (b : α i) :
a +ᵥ i, b⟩ = i, a +ᵥ b
@[simp]
theorem sigma.smul_mk {ι : Type u_1} {M : Type u_2} {α : ι → Type u_4} [Π (i : ι), (α i)] (a : M) (i : ι) (b : α i) :
a i, b⟩ = i, a b
@[protected, instance]
def sigma.is_scalar_tower {ι : Type u_1} {M : Type u_2} {N : Type u_3} {α : ι → Type u_4} [Π (i : ι), (α i)] [Π (i : ι), (α i)] [ N] [∀ (i : ι), (α i)] :
(Σ (i : ι), α i)
@[protected, instance]
def sigma.smul_comm_class {ι : Type u_1} {M : Type u_2} {N : Type u_3} {α : ι → Type u_4} [Π (i : ι), (α i)] [Π (i : ι), (α i)] [∀ (i : ι), (α i)] :
(Σ (i : ι), α i)
@[protected, instance]
def sigma.vadd_comm_class {ι : Type u_1} {M : Type u_2} {N : Type u_3} {α : ι → Type u_4} [Π (i : ι), (α i)] [Π (i : ι), (α i)] [∀ (i : ι), (α i)] :
(Σ (i : ι), α i)
@[protected, instance]
def sigma.is_central_scalar {ι : Type u_1} {M : Type u_2} {α : ι → Type u_4} [Π (i : ι), (α i)] [Π (i : ι), (α i)] [∀ (i : ι), (α i)] :
(Σ (i : ι), α i)
@[protected]
theorem sigma.has_faithful_vadd' {ι : Type u_1} {M : Type u_2} {α : ι → Type u_4} [Π (i : ι), (α i)] (i : ι) [ (α i)] :
(Σ (i : ι), α i)

This is not an instance because i becomes a metavariable.

@[protected]
theorem sigma.has_faithful_smul' {ι : Type u_1} {M : Type u_2} {α : ι → Type u_4} [Π (i : ι), (α i)] (i : ι) [ (α i)] :
(Σ (i : ι), α i)

This is not an instance because i becomes a metavariable.

@[protected, instance]
def sigma.has_faithful_smul {ι : Type u_1} {M : Type u_2} {α : ι → Type u_4} [Π (i : ι), (α i)] [nonempty ι] [∀ (i : ι), (α i)] :
(Σ (i : ι), α i)
@[protected, instance]
def sigma.has_faithful_vadd {ι : Type u_1} {M : Type u_2} {α : ι → Type u_4} [Π (i : ι), (α i)] [nonempty ι] [∀ (i : ι), (α i)] :
(Σ (i : ι), α i)
@[protected, instance]
def sigma.add_action {ι : Type u_1} {M : Type u_2} {α : ι → Type u_4} {m : add_monoid M} [Π (i : ι), (α i)] :
(Σ (i : ι), α i)
Equations
@[protected, instance]
def sigma.mul_action {ι : Type u_1} {M : Type u_2} {α : ι → Type u_4} {m : monoid M} [Π (i : ι), (α i)] :
(Σ (i : ι), α i)
Equations