instIsScalarTower — Mathlib

English

The scalar actions are compatible: for a ∈ 𝕜, b ∈ 𝕜′, f ∈ SchwartzMap, one has (a b) · f = a · (b · f) as functions.

Русский

Совместимы скалярные множители: (a b) · f = a · (b · f) как функции.

LaTeX

$$$ (a \\cdot b) \\cdot f = a \\cdot (b \\cdot f) $ (as functions)$$

Lean4

instance instIsScalarTower [SMul 𝕜 𝕜'] [IsScalarTower 𝕜 𝕜' F] : IsScalarTower 𝕜 𝕜' 𝓢(E, F) :=
  ⟨fun a b f => ext fun x => smul_assoc a b (f x)⟩

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