map_polynomialZ — Mathlib

English

Base change preserves the nonsingularity of the projective Weierstrass curve.

Русский

Изменение базы сохраняет несингулярность проективной кривой Вейерштраса.

LaTeX

$$$(W'.baseChange B).toProjective.Nonsingular = (W'.toProjective).Nonsingular$$$

Lean4

@[simp]
theorem map_polynomialZ : (W'.map f).toProjective.polynomialZ = MvPolynomial.map f W'.polynomialZ := by
  simp only [polynomialZ, map_polynomial, pderiv_map]

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