isScalarTower — Mathlib

English

The triple of scalar actions forms a scalar tower on the Lex-structured dependent functions, i.e., (r • (s • f)) = (r s) • f.

Русский

Тройка действий скаляров образует т Tower над Lex: (r • (s • f)) = (r s) • f.

LaTeX

$$$$ (r \\cdot (s \\cdot f)) = (r s) \\cdot f $$$$

Lean4

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

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