coeff_Ψ₂Sq_ne_zero

Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree

URI: https://scilib.ai/kg/mathlib#WeierstrassCurve.coeff_Ψ₂Sq_ne_zero

English

If the characteristic condition (4 ≠ 0) holds in R, then the coefficient of x^3 in Ψ₂Sq is nonzero.

Русский

При условии, что 4 не равно нулю в R, коэффициент полинома Ψ₂Sq перед x^3 не равен нулю.

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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