support_mul_subset_add_support — Mathlib

English

The product cannot create new exponents outside the sum of the individual supports.

Русский

Произведение не может создать новые степени за пределами суммы опор.

LaTeX

$$$\operatorname{supp}(x y) \subseteq \operatorname{supp}(x) + \operatorname{supp}(y)$$$

Lean4

theorem support_mul_subset_add_support [NonUnitalNonAssocSemiring R] {x y : HahnSeries Γ R} :
    support (x * y) ⊆ support x + support y :=
  by
  rw [← of_symm_smul_of_eq_mul, ← vadd_eq_add]
  exact HahnModule.support_smul_subset_vadd_support

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