nonsingularLift_some — Mathlib

English

For a,b in R, the nonsingularity of the lift of [a,b,1] corresponds to the affine nonsingularity of (a,b).

Русский

Для a,b ∈ R несингулярность лифта точки [a,b,1] соответствует аффинной несингулярности (a,b).

LaTeX

$$$W'.NonsingularLift\\langle a,b,1\\rangle \\iff W'.toAffine.Nonsingular(a,b)$$$

Lean4

theorem nonsingularLift_some (a b : R) : W'.NonsingularLift ⟦![a, b, 1]⟧ ↔ W'.toAffine.Nonsingular a b :=
  nonsingular_some a b

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