zsmul — Mathlib

English

If H is an AddSubgroup of an AddGroup G, then it is closed under integer scaling: for all a in H and n in Z, n•a ∈ H.

Русский

Если H — AddSubgroup в AddGroup G, то она замкнута относительно целочисленного масштабирования: для всех a ∈ H и n ∈ Z выполняется n•a ∈ H.

LaTeX

$$$\forall a \in H,\\forall n \in \mathbb{Z},\\ n \cdot a \in H$$$

Lean4

/-- An `AddSubgroup` of an `AddGroup` inherits an integer scaling. -/
instance _root_.AddSubgroup.zsmul {G} [AddGroup G] {H : AddSubgroup G} : SMul ℤ H :=
  ⟨fun n a => ⟨n • a, H.zsmul_mem a.2 n⟩⟩

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