nonsingular_iff_variableChange — Mathlib

English

The evaluation of polynomialX yields a linear expression in y: a1 y plus a quadratic in x plus a4 in x, up to standard terms.

Русский

Оценка polynomialX даёт линейную зависимость по y и квадратичную по x, в терминах коэффициентов a1,a2,a3,a4.

LaTeX

$$evalEval_polynomialX : W.polynomialX.evalEval x y = W.a₁ * y - (3 * x^2 + 2 * W.a₂ * x + W.a₄)$$

Lean4

theorem nonsingular_iff_variableChange (x y : R) :
    W.Nonsingular x y ↔ (VariableChange.mk 1 x 0 y • W).toAffine.Nonsingular 0 0 :=
  by
  rw [nonsingular_iff', equation_iff_variableChange, equation_zero, ← neg_ne_zero, or_comm, nonsingular_zero,
    variableChange_a₃, variableChange_a₄, inv_one, Units.val_one]
  simp only [variableChange_def]
  congr! 3 <;> ring1

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