English
If H is an AddSubgroup of an AddGroup G, then H is closed under natural scalar multiplication by natural numbers: for all a in H and n in N, n•a ∈ H.
Русский
Если H — AddSubgroup в AddGroup G, то H замкнута относительно скалярного умножения на натуральные числа: для всех a ∈ H и n ∈ ℕ выполняется n•a ∈ H.
LaTeX
$$$\forall a \in H,\\forall n \in \mathbb{N},\\ n \cdot a \in H$$$
Lean4
/-- An `AddSubgroup` of an `AddGroup` inherits a natural scaling. -/
instance _root_.AddSubgroup.nsmul {G} [AddGroup G] {H : AddSubgroup G} : SMul ℕ H :=
⟨fun n a => ⟨n • a, H.nsmul_mem a.2 n⟩⟩