support_zsmul — Mathlib

English

Scaling by a nonzero integer does not change the support.

Русский

Умножение на ненулевое целое не изменяет опору.

LaTeX

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

Lean4

@[simp]
theorem support_zsmul (k : ℤ) (h : k ≠ 0) (a : FreeAbelianGroup X) : support (k • a) = support a :=
  by
  ext x
  simp only [mem_support_iff, AddMonoidHom.map_zsmul]
  simp only [h, zsmul_int_int, false_or, Ne, mul_eq_zero]

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