nonsingularLift_iff — Mathlib

English

Let R be a commutative ring and W' a Jacobian over R. For any polynomial P: Fin 3 → R, the lifted nonsingularity of the class of P equals the nonsingularity of P itself on W'.

Русский

Пусть R — коммутативное кольцо и W' — якобиан над R. Для любого P: Fin 3 → R равносильна безсингулярность подъёма класса P и несингуларность самого P на W'.

LaTeX

$$$$W'\\,\\mathrm{NonsingularLift}(\\overline{P}) \\iff W'\\mathrm{Nonsingular}(P)$$$$

Lean4

theorem nonsingularLift_iff (P : Fin 3 → R) : W'.NonsingularLift ⟦P⟧ ↔ W'.Nonsingular P :=
  Iff.rfl

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