nonsingular_iff_of_Z_ne_zero — Mathlib

English

There is an equivalence between W.Nonsingular P and a conjunction of W.Equation P and nonvanishing of certain affine coordinates when P z ≠ 0.

Русский

Существует эквивалентность между неособостью P и сочетанием уравнения кривой и ненулевой аффинной оценки координат при P z ≠ 0.

LaTeX

$$$ W.Nonsingular P \\iff W.Equation P \\wedge (\\mathrm{eval} P W.polynomialX \\neq 0 \\lor \\mathrm{eval} P W.polynomialY \\neq 0) $$$

Lean4

theorem nonsingular_iff_of_Z_ne_zero {P : Fin 3 → F} (hPz : P z ≠ 0) :
    W.Nonsingular P ↔ W.Equation P ∧ (eval P W.polynomialX ≠ 0 ∨ eval P W.polynomialY ≠ 0) := by
  rw [nonsingular_of_Z_ne_zero hPz, Affine.Nonsingular, ← equation_of_Z_ne_zero hPz, ←
    eval_polynomialX_of_Z_ne_zero hPz, div_ne_zero_iff, and_iff_left <| pow_ne_zero 4 hPz, ←
    eval_polynomialY_of_Z_ne_zero hPz, div_ne_zero_iff, and_iff_left <| pow_ne_zero 3 hPz]

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