isCentralScalar — Mathlib

English

The scalar action on the Lex space is central, i.e., left scalar action commutes with right scalar actions on each coordinate.

Русский

Действие скаляра над пространством Lex центрально: левое действие скаляра коммутирует с правым действием на каждой координате.

LaTeX

$$$$ \\text{IsCentralScalar}(\\\\gamma, (β_i)) $$$$

Lean4

instance isCentralScalar [∀ i, Zero (β i)] [∀ i, SMulZeroClass γ (β i)] [∀ i, SMulZeroClass γᵐᵒᵖ (β i)]
    [∀ i, IsCentralScalar γ (β i)] : IsCentralScalar γ (Π₀ i, β i) where
  op_smul_eq_smul r m := ext fun i => by simp only [smul_apply, op_smul_eq_smul r (m i)]

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