Φ_ne_zero — Mathlib

English

For a Weierstrass curve W over a nontrivial ring R, for every integer n, the polynomial W.Φ(n) is nonzero.

Русский

Для кривая Вейерштрасса W над не тривиальным кольцом R для любого целого n полином W.Φ(n) не равен нулю.

LaTeX

$$$W.\Phi(n) \neq 0$$$

Lean4

theorem Φ_ne_zero [Nontrivial R] (n : ℤ) : W.Φ n ≠ 0 :=
  by
  by_cases hn : n = 0
  · simpa only [hn, Φ_zero] using one_ne_zero
  · exact ne_zero_of_natDegree_gt <| W.natDegree_Φ_pos hn

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