leadingCoeff_preΨ₄

Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree

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

English

If 2 ≠ 0, the leading coefficient of preΨ4 is 2.

Русский

Если 2 ≠ 0, то ведущий коэффициент preΨ4 равен 2.

LaTeX

$$(2 \neq 0) \Rightarrow (W.preΨ_4).leadingCoeff = 2$$

Lean4

@[simp]
theorem leadingCoeff_preΨ₄ (h : (2 : R) ≠ 0) : W.preΨ₄.leadingCoeff = 2 := by
  rw [leadingCoeff, W.natDegree_preΨ₄ h, coeff_preΨ₄]

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

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

Разделы

Аффилиация

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