equation_iff_variableChange — Mathlib

English

At the origin (0,0), nonsingularity is equivalent to a6=0 and either a3 ≠ 0 or a4 ≠ 0.

Русский

В точке (0,0) невырожденность эквивалентна a6=0 и либо a3 ≠ 0, либо a4 ≠ 0.

LaTeX

$$W.Nonsingular 0 0 ↔ W.a₆ = 0 ∧ (W.a₃ ≠ 0 ∨ W.a₄ ≠ 0)$$

Lean4

theorem equation_iff_variableChange (x y : R) :
    W.Equation x y ↔ (VariableChange.mk 1 x 0 y • W).toAffine.Equation 0 0 :=
  by
  rw [equation_iff', ← neg_eq_zero, equation_zero, variableChange_a₆, inv_one, Units.val_one]
  congr! 1
  ring1

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