nonsingular_of_equiv — Mathlib

English

If P is equivalent to Q under the Weierstrass Jacobian relation, then nonsingularity of P is equivalent to nonsingularity of Q.

Русский

Если P эквивалентно Q в рамках эквив-отношения Якобиана, то неособость P и Q эквивалентны.

LaTeX

$$$ W'.Nonsingular P \\leftrightarrow W'.Nonsingular Q \\text{ whenever } P \\approx Q $$$

Lean4

theorem nonsingular_of_equiv {P Q : Fin 3 → R} (h : P ≈ Q) : W'.Nonsingular P ↔ W'.Nonsingular Q :=
  by
  rcases h with ⟨u, rfl⟩
  exact nonsingular_smul Q u.isUnit

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