support_nsmul — Mathlib

English

Multiplication by a positive natural number nonzero preserves the support.

Русский

Умножение на ненулевое натуральное число сохраняет опору.

LaTeX

$$$\\forall k \\in \\mathbb{N}, k \\neq 0:\\; \\operatorname{support}(k \\cdot a) = \\operatorname{support}(a)$$$

Lean4

@[simp]
theorem support_nsmul (k : ℕ) (h : k ≠ 0) (a : FreeAbelianGroup X) : support (k • a) = support a :=
  by
  apply support_zsmul k _ a
  exact mod_cast h

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