degree_mono

Mathlib.Algebra.Polynomial.Degree.Definitions

URI: https://scilib.ai/kg/mathlib#Polynomial.degree_mono

English

If f is supported inside g, then deg f ≤ deg g.

Русский

Если поддержка f ⊆ поддержке g, то deg f ≤ deg g.

LaTeX

$$$\deg(f) \le \deg(g)$ whenever $\operatorname{supp}(f) \subseteq \operatorname{supp}(g)$$$

Lean4

theorem degree_mono [Semiring S] {f : R[X]} {g : S[X]} (h : f.support ⊆ g.support) : f.degree ≤ g.degree :=
  Finset.sup_mono h

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

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

Разделы

Аффилиация

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