natDegree_ΨSq_pos — Mathlib

English

Let R be a commutative ring with no zero divisors and W a Weierstrass curve over R. If n ∈ Z satisfies |n| > 1 and (n : R) ≠ 0, then the division polynomial ΨSq(n) has positive degree. In particular, natDegree(W.ΨSq n) > 0.

Русский

Пусть R — коммутативное кольцо без нулевых делителей, и W — кривая Вейерштрасса над R. Пусть n ∈ Z таково, что |n| > 1 и (n : R) ≠ 0. Тогда полином ΨSq(n) имеет положительную степень: natDegree(W.ΨSq n) > 0.

LaTeX

$$$0 < \operatorname{natDegree}\bigl(W.\PsiSq(n)\bigr)$$$

Lean4

theorem natDegree_ΨSq_pos [NoZeroDivisors R] {n : ℤ} (hn : 1 < n.natAbs) (h : (n : R) ≠ 0) : 0 < (W.ΨSq n).natDegree :=
  by simpa [W.natDegree_ΨSq h]

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