natTrailingDegree_mem_support_of_nonzero

Mathlib.Algebra.Polynomial.Degree.TrailingDegree

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

← MathLib Explorer

English

If p ≠ 0, then natTrailingDegree(p) ∈ p.support.

Русский

Если p ≠ 0, то natTrailingDegree(p) принадлежит support(p).

LaTeX

$$p \neq 0 \Rightarrow \operatorname{natTrailingDegree}(p) \in p.support$$

Lean4

theorem natTrailingDegree_mem_support_of_nonzero : p ≠ 0 → natTrailingDegree p ∈ p.support :=
  mem_support_iff.mpr ∘ trailingCoeff_nonzero_iff_nonzero.mpr

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

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

Разделы

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

Аффилиация

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