natTrailingDegree_eq_of_trailingDegree_eq_some

Mathlib.Algebra.Polynomial.Degree.TrailingDegree

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

← MathLib Explorer

English

If trailingDegree(p) = n for some n, then natTrailingDegree(p) = n.

Русский

Если хвостовая степень p равна n, то natTrailingDegree(p) = n.

LaTeX

$$$\operatorname{trailingDegree}(p) = n \Rightarrow \operatorname{natTrailingDegree}(p) = n$$$

Lean4

theorem natTrailingDegree_eq_of_trailingDegree_eq_some {p : R[X]} {n : ℕ} (h : trailingDegree p = n) :
    natTrailingDegree p = n := by simp [natTrailingDegree, h]

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

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

Разделы

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

Аффилиация

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