natDegree_Φ_le — Mathlib

English

For a Weierstrass curve W over a ring R, the polynomial Φ(n) has degree at most |n|^2 for every integer n.

Русский

Для кривая Вейерштрасса W над кольцом R полином Φ(n) имеет степень не превосходящую |n|^2 для каждого целого n.

LaTeX

$$$\operatorname{natDegree}\bigl(W.\Φ(n)\bigr) \le (n.natAbs)^2$$$

Lean4

theorem natDegree_Φ_le (n : ℤ) : (W.Φ n).natDegree ≤ n.natAbs ^ 2 := by
  induction n using Int.negInduction with
  | nat n => exact (W.natDegree_coeff_Φ_ofNat n).left
  | neg ih => simp_rw [Φ_neg, Int.natAbs_neg, ih]

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