instIsScalarTower — Mathlib

English

There is a scalar-tower compatibility: smul_assoc holds pointwise for ZeroAtInftyContinuousMap.

Русский

Содержится совместимость скалярного тTower: smul_assoc выполняется по точкам для ZeroAtInftyContinuousMap.

LaTeX

$$IsScalarTower R (ZeroAtInftyContinuousMap α β) (ZeroAtInftyContinuousMap α β). smul_assoc holds.$$

Lean4

instance instIsScalarTower {R : Type*} [Semiring R] [NonUnitalNonAssocSemiring β] [IsTopologicalSemiring β] [Module R β]
    [ContinuousConstSMul R β] [IsScalarTower R β β] : IsScalarTower R 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]

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