leadingCoeff_Ψ₃

Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree

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

English

Under 3 ≠ 0, the leading coefficient of Ψ₃ is 3.

Русский

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

LaTeX

$$$ W.\\Psi_3.leadingCoeff = 3 $$$

Lean4

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

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

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

Разделы

Аффилиация

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