YClass_ne_zero — Mathlib

English

Let R be a nontrivial commutative ring and W' an affine Weierstrass curve over R. Then for every polynomial y in R[X], the element YClass(W', y) is nonzero in the coordinate ring.

Русский

Пусть R — не нулевой коммутативный кольцо, и W' — аффинная кривая Вейерштрасса над R. Тогда для любого полинома y ∈ R[X] элемент YClass(W', y) ненулевой в координатной кольце.

LaTeX

$$$\forall R [\text{CommRing }R],\ \forall W'\!:\!\mathrm{WeierstrassCurve.Affine}(R),\ \forall y\in R[X],\ YClass(W', y) \neq 0$$$

Lean4

theorem YClass_ne_zero [Nontrivial R] (y : R[X]) : YClass W' y ≠ 0 :=
  AdjoinRoot.mk_ne_zero_of_natDegree_lt monic_polynomial (X_sub_C_ne_zero y) <| by
    rw [natDegree_polynomial, natDegree_X_sub_C]; norm_num1

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