nsmul — Mathlib

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

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