natDegree_Φ_pos

Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree

URI: https://scilib.ai/kg/mathlib#WeierstrassCurve.natDegree_Φ_pos

English

For a Weierstrass curve W over a nontrivial ring R and any nonzero integer n, the polynomial W.Φ(n) has positive degree.

Русский

При не нуль-цикле R и любом не нулевом целым n полином W.Φ(n) имеет положительную степень.

LaTeX

$$$0 < (W.\Φ(n)).natDegree$ при $n \neq 0$$$

Lean4

theorem natDegree_Φ_pos [Nontrivial R] {n : ℤ} (hn : n ≠ 0) : 0 < (W.Φ n).natDegree := by simpa [sq_pos_iff]

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

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

Разделы

Аффилиация

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