natDegree_preΨ₄_pos

Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree

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

English

Under 2 ≠ 0, the degree of preΨ4 is positive.

Русский

При условии 2 ≠ 0 deg preΨ4 положительно.

LaTeX

$$(2 \neq 0) \Rightarrow 0 < \operatorname{natDegree}(W.preΨ_4)$$

Lean4

theorem natDegree_preΨ₄_pos (h : (2 : R) ≠ 0) : 0 < W.preΨ₄.natDegree := by linarith only [W.natDegree_preΨ₄ h]

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

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

Разделы

Аффилиация

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