zsmul — Mathlib

English

An additive subgroup inherits an action of the integers: for every integer n and every a in H, n • a ∈ H.

Русский

Аддитивная подгруппа наследует действие целых чисел: для каждого n ∈ ℤ и каждого a ∈ H выполняется n • a ∈ H.

LaTeX

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

Lean4

/-- An additive subgroup of an `AddGroup` inherits an integer scaling. -/
instance _root_.AddSubgroupClass.zsmul {M S} [SubNegMonoid M] [SetLike S M] [AddSubgroupClass S M] {H : S} : SMul ℤ H :=
  ⟨fun n a => ⟨n • a.1, zsmul_mem a.2 n⟩⟩

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