natDegree_preΨ₄

Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree

URI: https://scilib.ai/kg/mathlib#WeierstrassCurve.natDegree_preΨ₄

← MathLib Explorer

English

If 2 is nonzero in R, then the natDegree of preΨ4 equals 6.

Русский

Если 2 не равно нулю в R, то естественная степень preΨ4 равна 6.

LaTeX

$$(2 \neq 0) \Rightarrow \operatorname{natDegree}(W.preΨ_4) = 6$$

Lean4

@[simp]
theorem natDegree_preΨ₄ (h : (2 : R) ≠ 0) : W.preΨ₄.natDegree = 6 :=
  natDegree_eq_of_le_of_coeff_ne_zero W.natDegree_preΨ₄_le <| W.coeff_preΨ₄_ne_zero h

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

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

Разделы

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

Аффилиация

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