nonsingular_iff_of_Y_eq_negY — Mathlib

English

A projective point P is nonsingular on W iff P satisfies the curve equation and the X-polynomial evaluated at P is nonzero, provided P_y equals negY P.

Русский

Проективная точка P безразлична к невырожденности на W тогда и только тогда, когда P удовлетворяет уравнение кривой и A-коэффициент X не равен 0, при условии P_y = negY P.

LaTeX

$$$ W.Nonsingular P \\iff W.Equation P \\land eval\\ P\\ W.polynomialX \\neq 0 $$$

Lean4

theorem nonsingular_iff_of_Y_eq_negY {P : Fin 3 → F} (hPz : P z ≠ 0) (hy : P y = W.negY P) :
    W.Nonsingular P ↔ W.Equation P ∧ eval P W.polynomialX ≠ 0 :=
  by
  have hy' : eval P W.polynomialY = (P y - W.negY P) * P z := by rw [negY, eval_polynomialY]; ring1
  rw [nonsingular_iff_of_Z_ne_zero hPz, hy', hy, sub_self, zero_mul, ne_self_iff_false, or_false]

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