nsmul — Mathlib

English

The natural-scalar action of the natural numbers on NormedAddGroupHom is defined by repeated addition.

Русский

Действие натурального числа на NormedAddGroupHom определяется повторяющимся сложением.

LaTeX

$$$$ \text{natural-scalar action: } n \cdot f = f + f + \cdots + f \ (n \text{ times}) $$$$

Lean4

instance nsmul : SMul ℕ (NormedAddGroupHom V₁ V₂) where
  smul n
    f :=
    { toFun := n • ⇑f
      map_add' := (n • f.toAddMonoidHom).map_add'
      bound' :=
        let ⟨b, hb⟩ := f.bound'
        ⟨n • b, fun v => by
          rw [Pi.smul_apply, nsmul_eq_mul, mul_assoc]
          exact norm_nsmul_le.trans (by gcongr; apply hb)⟩ }

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