nonsingular_of_Z_eq_zero — Mathlib

English

If P z = 0, then W'.Nonsingular P is equivalent to W'.Equation P together with a nonvanishing among 3 P x^2, 2 P y, and a1 P x P y.

Русский

Если P z = 0, то W'.Nonsingular P эквивалентно W'.Equation P и неравенству по 3 P x^2, 2 P y, или a1 P x P y.

LaTeX

$$$ W'.Nonsingular P \\leftrightarrow W'.Equation P \\wedge (3 \\cdot P x^{2} \\neq 0 \\lor 2 \\cdot P y \\neq 0 \\lor W'.a_1 \\cdot P x \\cdot P y \\neq 0)$$$

Lean4

theorem nonsingular_of_Z_eq_zero {P : Fin 3 → R} (hPz : P z = 0) :
    W'.Nonsingular P ↔ W'.Equation P ∧ (3 * P x ^ 2 ≠ 0 ∨ 2 * P y ≠ 0 ∨ W'.a₁ * P x * P y ≠ 0) := by
  simp only [nonsingular_iff, hPz, add_zero, sub_zero, zero_sub, mul_zero, zero_pow <| OfNat.ofNat_ne_zero _,
    neg_ne_zero]

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