nonsingular_some — Mathlib

English

If P z ≠ 0, then W.Nonsingular P is equivalent to W.toAffine.Nonsingular (P x / P z^2) (P y / P z^3).

Русский

Если P z ≠ 0, то неособость в полного Якобиана эквивалентна неособости в аффинной модели с нормализованными координатами.

LaTeX

$$$ W.Nonsingular P \\iff W.toAffine.Nonsingular (P x / P z^{2}) (P y / P z^{3}) $$$

Lean4

theorem nonsingular_some (a b : R) : W'.Nonsingular ![a, b, 1] ↔ W'.toAffine.Nonsingular a b :=
  by
  simp_rw [nonsingular_iff, equation_some, fin3_def_ext, Affine.nonsingular_iff', Affine.equation_iff',
    and_congr_right_iff, ← not_and_or, not_iff_not, one_pow, mul_one, and_congr_right_iff, Iff.comm, iff_self_and]
  intro h ha hb
  linear_combination (norm := ring1) 6 * h - 2 * a * ha - 3 * b * hb

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