natDegree_preΨ₄_le — Mathlib

English

Let W be a Weierstrass curve over a commutative ring R. Then the division polynomial preΨ4 has natural degree at most 6.

Русский

Пусть W — кривая Вайерштрасса над коммутативным кольцом R. Тогда полином деления preΨ₄ имеет натуральную степень не более 6.

LaTeX

$$$\operatorname{natDegree}(W.preΨ_4) \le 6$$$

Lean4

theorem natDegree_preΨ₄_le : W.preΨ₄.natDegree ≤ 6 := by
  rw [preΨ₄]
  compute_degree

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