instSMulNat — Mathlib

English

There is a natural action of the natural numbers on kernels: for all n ∈ ℕ and κ, (n • κ)(a) = n • (κ a).

Русский

Существует естественное действие натуральных чисел на ядрах: для всех n ∈ ℕ и κ выполняется (n • κ)(a) = n • (κ a).

LaTeX

$$$\forall n\in\mathbb{N}, \forall a, (n \cdot \kappa) a = n \cdot (\kappa a)$$$

Lean4

noncomputable instance instSMulNat : SMul ℕ (Kernel α β) where smul n κ := ⟨n • κ, (measurable_const (a := n)).smul κ.2⟩

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