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)⟩ }