degree_eq

Mathlib.Algebra.Polynomial.Sequence

URI: https://scilib.ai/kg/mathlib#Polynomial.Sequence.degree_eq

English

For a polynomial sequence S, the i-th element S i has degree i.

Русский

Для последовательности многочленов S элемент S i имеет степень i.

LaTeX

$$$\forall i\in\mathbb{N},\; \operatorname{deg}(S(i)) = i$$$

Lean4

/-- `S i` has degree `i`. -/
@[simp]
theorem degree_eq (i : ℕ) : (S i).degree = i :=
  S.degree_eq' i

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

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

Разделы

Аффилиация

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