instIsScalarTower — Mathlib

English

Let R be a semiring and β a topological semiring which is an R-module with continuous scalar action. Then C_c(α, β) forms a scalar tower, i.e., for r∈R, f,g ∈ C_c(α,β), (r·f)·g = r·(f·g).

Русский

Пусть R — полупринод; β — топологическое полупольное кольцо, модуль над R с непрерывным действием скаляра. Тогда C_c(α, β) образует скалярную башню: (r·f)·g = r·(f·g) для всех r∈R и f,g∈C_c(α,β).

LaTeX

$$$IsScalarTower(R, C_c(α,β), C_c(α,β))$$$

Lean4

instance {R : Type*} [Semiring R] [NonUnitalNonAssocSemiring β] [IsTopologicalSemiring β] [Module R β]
    [ContinuousConstSMul R β] [IsScalarTower R β β] : IsScalarTower R C_c(α, β) C_c(α, β) where
  smul_assoc r f
    g := by
    ext
    simp only [smul_eq_mul, coe_mul, coe_smul, Pi.mul_apply, Pi.smul_apply]
    rw [← smul_eq_mul, ← smul_eq_mul, smul_assoc]

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