natDegree_Ψ₂Sq

Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree

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

← MathLib Explorer

English

If 4 ≠ 0 in R, then the degree of Ψ₂Sq is exactly 3.

Русский

Если 4 не равно нулю в R, то степень Ψ₂Sq равна 3.

LaTeX

$$$ W.\\Ψ_2Sq.natDegree = 3 $$$

Lean4

@[simp]
theorem natDegree_Ψ₂Sq (h : (4 : R) ≠ 0) : W.Ψ₂Sq.natDegree = 3 :=
  natDegree_eq_of_le_of_coeff_ne_zero W.natDegree_Ψ₂Sq_le <| W.coeff_Ψ₂Sq_ne_zero h

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

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

Разделы

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

Аффилиация

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