nonsingular_iff_of_Y_eq_negY — Mathlib

English

Let P be a Fin 3 → F with P_z ≠ 0 and hy = P_y = W.negY P. Then W.Nonsingular P holds iff W.Equation P and eval P W.polynomialX ≠ 0.

Русский

Пусть P задана на Fin(3) с P_z ≠ 0 и P_y = W.negY P. Тогда W.Nonsingular P эквивалентно W.Equation P и eval P W.polynomialX ≠ 0.

LaTeX

$$$P_z \neq 0 \land P_y = W.negY P \Rightarrow (W.Nonsingular P \,\Leftrightarrow\, (W.Equation P) \land eval P W.polynomialX \neq 0)$$$

Lean4

theorem nonsingular_iff_of_Y_eq_negY {P : Fin 3 → F} (hPz : P z ≠ 0) (hy : P y = W.negY P) :
    W.Nonsingular P ↔ W.Equation P ∧ eval P W.polynomialX ≠ 0 :=
  by
  have hy' : eval P W.polynomialY = P y - W.negY P := by rw [negY, eval_polynomialY]; ring1
  rw [nonsingular_iff_of_Z_ne_zero hPz, hy', hy, sub_self, ne_self_iff_false, or_false]

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