natDegree_eq

Mathlib.Algebra.Polynomial.Sequence

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

English

For the i-th element, natDegree equals i.

Русский

Для i-го элемента natDegree равен i.

LaTeX

$$$\forall i,\; (S(i)).natDegree = i$$$

Lean4

/-- `S i` has `natDegree` `i`. -/
@[simp]
theorem natDegree_eq (i : ℕ) : (S i).natDegree = i :=
  natDegree_eq_of_degree_eq_some <| S.degree_eq i

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

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

Разделы

Аффилиация

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