natDegree_Ψ₃

Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree

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

← MathLib Explorer

English

Assuming 3 ≠ 0, the degree of Ψ₃ is 4.

Русский

При условии 3 ≠ 0 степень Ψ₃ равна 4.

LaTeX

$$$ W.\\Psi_3.natDegree = 4 $$$

Lean4

@[simp]
theorem natDegree_Ψ₃ (h : (3 : R) ≠ 0) : W.Ψ₃.natDegree = 4 :=
  natDegree_eq_of_le_of_coeff_ne_zero W.natDegree_Ψ₃_le <| W.coeff_Ψ₃_ne_zero h

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

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

Разделы

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

Аффилиация

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