natDegree_mem_support_of_nonzero

Mathlib.Algebra.Polynomial.Degree.Support

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

← MathLib Explorer

English

If p ≠ 0, then natDegree(p) is an element of the support of p.

Русский

Если p ≠ 0, то natDegree(p) ∈ поддержка(p).

LaTeX

$$$p \neq 0 \Rightarrow \operatorname{natDegree}(p) \in \operatorname{supp}(p).$$$

Lean4

theorem natDegree_mem_support_of_nonzero (H : p ≠ 0) : p.natDegree ∈ p.support :=
  by
  rw [mem_support_iff]
  exact (not_congr leadingCoeff_eq_zero).mpr H

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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