nonsingular_iff — Mathlib

English

Scaling by a unit preserves nonsingularity: W'.Nonsingular P implies W'.Nonsingular (u · P) for unit u, and conversely.

Русский

Умножение на единицу сохраняет невырожденность: W'.Nonsingular P влечёт W'.Nonsingular (u · P) при единице u и обратно.

LaTeX

$$$W'.Nonsingular P \\-\\to W'.Nonsingular (u P) \\quad\\text{and}\\quad W'.Nonsingular (u P) \\to W'.Nonsingular P$$

Lean4

theorem nonsingular_iff (P : Fin 3 → R) :
    W'.Nonsingular P ↔
      W'.Equation P ∧
        (W'.a₁ * P y * P z - (3 * P x ^ 2 + 2 * W'.a₂ * P x * P z + W'.a₄ * P z ^ 2) ≠ 0 ∨
          2 * P y * P z + W'.a₁ * P x * P z + W'.a₃ * P z ^ 2 ≠ 0 ∨
            P y ^ 2 + W'.a₁ * P x * P y + 2 * W'.a₃ * P y * P z -
                (W'.a₂ * P x ^ 2 + 2 * W'.a₄ * P x * P z + 3 * W'.a₆ * P z ^ 2) ≠
              0) :=
  by rw [Nonsingular, eval_polynomialX, eval_polynomialY, eval_polynomialZ]

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