le_inf_support_finset_prod — Mathlib

English

If the support of a polynomial contains a maximum degree element, the corresponding coefficient is nonzero and uniquely determines that degree in the sup-degree.

Русский

Если в поддержке полинома есть максимальная степень, её коэффициент не равен нулю и определяет соответствующую степень в верхней грани.

LaTeX

$$$\\exists a: A, a\\in\\operatorname{Supp}(f) \\land \\text{IsMaxOn}(D,\\operatorname{Supp}(f), a)\\Rightarrow \\supDegree D f = D a$$$

Lean4

theorem le_inf_support_finset_prod (degt0 : 0 ≤ degt 0) (degtm : ∀ a b, degt a + degt b ≤ degt (a + b)) (s : Finset ι)
    (f : ι → R[A]) : (∑ i ∈ s, (f i).support.inf degt) ≤ (∏ i ∈ s, f i).support.inf degt :=
  le_of_eq_of_le (by rw [Multiset.map_map]; rfl) (le_inf_support_multiset_prod degt0 degtm _)

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