natDegree_ΨSq

Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree

URI: https://scilib.ai/kg/mathlib#WeierstrassCurve.natDegree_ΨSq

← MathLib Explorer

English

For any NoZeroDivisors ring and n ≠ 0, natDegree(W.ΨSq n) = n.natAbs^2 − 1.

Русский

Для кольца без нулевых делителей и n ≠ 0, natDegree(W.ΨSq n) = n^2 − 1.

LaTeX

$$natDegree(W.ΨSq n) = n.natAbs^2 - 1$$

Lean4

@[simp]
theorem natDegree_ΨSq [NoZeroDivisors R] {n : ℤ} (h : (n : R) ≠ 0) : (W.ΨSq n).natDegree = n.natAbs ^ 2 - 1 :=
  natDegree_eq_of_le_of_coeff_ne_zero (W.natDegree_ΨSq_le n) <| W.coeff_ΨSq_ne_zero h

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

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

Разделы

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

Аффилиация

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