support_smul

Mathlib.Algebra.DirectSum.Module

URI: https://scilib.ai/kg/mathlib#DirectSum.support_smul

English

The support of c • v is contained in the support of v: supp(c v) ⊆ supp(v).

Русский

Опора $c\\cdot v\$ содержится в опоре $v$: supp(c v) ⊆ supp(v).

LaTeX

$$$\\mathrm{supp}(c\\cdot v) \\subseteq \\mathrm{supp}(v).$$$

Lean4

theorem support_smul [∀ (i : ι) (x : M i), Decidable (x ≠ 0)] (c : R) (v : ⨁ i, M i) : (c • v).support ⊆ v.support :=
  DFinsupp.support_smul _ _

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru