trailingDegree_ne_of_natTrailingDegree_ne

Mathlib.Algebra.Polynomial.Degree.TrailingDegree

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

← MathLib Explorer

English

If natTrailingDegree(p) ≠ n, then trailingDegree(p) ≠ n.

Русский

Если natTrailingDegree(p) ≠ n, то trailingDegree(p) ≠ n.

LaTeX

$$$\operatorname{natTrailingDegree}(p) \neq n \Rightarrow \operatorname{trailingDegree}(p) \neq (n : \mathbb{N}_\infty)$$$

Lean4

theorem trailingDegree_ne_of_natTrailingDegree_ne {n : ℕ} : p.natTrailingDegree ≠ n → trailingDegree p ≠ n :=
  mt fun h => by rw [natTrailingDegree, h, ENat.toNat_coe]

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

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

Разделы

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

Аффилиация

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