nonsingular_some — Mathlib

English

For any a,b in R, the point [a,b,1] on W′ is nonsingular if and only if it satisfies the affine nonsingularity condition for (a,b).

Русский

Для любых a,b из R точка \$[a,b,1]\$ на W′ несингулярна тогда и только тогда, когда она удовлетворяет аффинному условию несингулярности для (a,b).

LaTeX

$$$a,b\\in R \\;\\Rightarrow\\; W'.Nonsingular([a,b,1]) \\iff W'.toAffine.Nonsingular(a,b)$$$

Lean4

theorem nonsingular_some (a b : R) : W'.Nonsingular ![a, b, 1] ↔ W'.toAffine.Nonsingular a b :=
  by
  simp_rw [nonsingular_iff, equation_some, fin3_def_ext, Affine.nonsingular_iff', Affine.equation_iff',
    and_congr_right_iff, ← not_and_or, not_iff_not, one_pow, mul_one, and_congr_right_iff, Iff.comm, iff_self_and]
  intro h ha hb
  linear_combination (norm := ring1) 3 * h - a * ha - b * hb

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