Y_ne_zero_of_Z_eq_zero — Mathlib

English

Over a NoZeroDivisors ring R, if W′ is nonsingular at P and P_z = 0, then the middle coordinate P_y must be nonzero.

Русский

В кольце без нулевых делителей R, если W′ несингулярна в P и P_z = 0, то координата Y тройки P не может быть равна нулю.

LaTeX

$$$[NoZeroDivisors\\ R] \\;{P:\\mathrm{Fin}(3)\\to R},\\; h_P\\!:\\ W'.Nonsingular P,\\; hPz:\\ P_z=0 \\Rightarrow P_y \\neq 0$$$

Lean4

theorem Y_ne_zero_of_Z_eq_zero [NoZeroDivisors R] {P : Fin 3 → R} (hP : W'.Nonsingular P) (hPz : P z = 0) : P y ≠ 0 :=
  by
  intro hPy
  simp only [nonsingular_of_Z_eq_zero hPz, X_eq_zero_of_Z_eq_zero hP.left hPz, hPy, add_zero, sub_zero, mul_zero,
    zero_pow two_ne_zero, or_self, ne_self_iff_false, and_false] at hP

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