smulCommClass — Mathlib

English

For scalar actions by γ and δ that commute coordinatewise, the product space DFinsupp(β_i) also respects the commuting scalar actions.

Русский

При коммутирующем по координатам действии скаляров γ и δ на β_i, произведение DFinsupp(β_i) сохраняет свойство коммутативности действий скаляров.

LaTeX

$$$$ \\text{SMulCommClass}(\\gamma,\\delta, (\\\\Pi_i β_i)) $$$$

Lean4

instance smulCommClass {δ : Type*} [∀ i, Zero (β i)] [∀ i, SMulZeroClass γ (β i)] [∀ i, SMulZeroClass δ (β i)]
    [∀ i, SMulCommClass γ δ (β i)] : SMulCommClass γ δ (Π₀ i, β i) where
  smul_comm r s m := ext fun i => by simp only [smul_apply, smul_comm r s (m i)]

Похожие утверждения