leadingCoeff_Ψ₂Sq

Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree

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

English

Under 4 ≠ 0, the leading coefficient of Ψ₂Sq is 4.

Русский

При 4 ≠ 0 ведущий коэффициент Ψ₂Sq равен 4.

LaTeX

$$$ W.\\Psi_2Sq.leadingCoeff = 4 $$$

Lean4

@[simp]
theorem leadingCoeff_Ψ₂Sq (h : (4 : R) ≠ 0) : W.Ψ₂Sq.leadingCoeff = 4 := by
  rw [leadingCoeff, W.natDegree_Ψ₂Sq h, coeff_Ψ₂Sq]

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

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

Разделы

Аффилиация

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