support_map_subset — Mathlib

English

The support of the coefficient-mapped polynomial is contained in the support of the original polynomial: supp(map_f p) ⊆ supp(p).

Русский

Опора полинома после отображения коэффициентов содержится в опоре исходного полинома: supp(map_f p) ⊆ supp(p).

LaTeX

$$$\\\\mathrm{supp}(\\\\mathrm{map}_f p) \\\\subseteq \\\\mathrm{supp}(p)$$$

Lean4

theorem support_map_subset (p : MvPolynomial σ R) : (map f p).support ⊆ p.support :=
  by
  simp only [Finset.subset_iff, mem_support_iff]
  intro x hx
  contrapose! hx
  rw [coeff_map, hx, RingHom.map_zero]

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