baseChange_addPolynomial — Mathlib

English

Under a base change, negY is preserved by mapping with AlgHom.

Русский

При базовом изменении negY сохраняется под отображением.

LaTeX

$$$ (W'.baseChange W).toAffine.negY (f x) (f y) = f (W'.negY x y) $$$

Lean4

theorem baseChange_addPolynomial :
    (W'.baseChange B).toAffine.addPolynomial (f x) (f y) (f ℓ) =
      ((W'.baseChange A).toAffine.addPolynomial x y ℓ).map f :=
  by rw [← RingHom.coe_coe, ← map_addPolynomial, map_baseChange]

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