coeff_Ψ₃_ne_zero

Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree

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

English

If h ≠ 0 with h ∈ R for 3, then the coefficient of x^4 in Ψ₃ is nonzero.

Русский

Если 3 не равно 0 и h ∈ R, тогда коэффициент x^4 в Ψ₃ не равен нулю.

LaTeX

$$$ (3 : R) \\neq 0 \\Rightarrow W.\\Psi_3.coeff 4 \\neq 0 $$$

Lean4

theorem coeff_Ψ₃_ne_zero (h : (3 : R) ≠ 0) : W.Ψ₃.coeff 4 ≠ 0 := by rwa [coeff_Ψ₃]

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

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

Разделы

Аффилиация

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