baseChange_negPolynomial — Mathlib

English

The negY operation commutes with base-change along AlgHom f from S to A to B.

Русский

Операция negY commute с базовым изменением через AlgHom.

LaTeX

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

Lean4

theorem baseChange_negPolynomial :
    (W'.baseChange B).toAffine.negPolynomial = (W'.baseChange A).toAffine.negPolynomial.map (mapRingHom f) := by
  rw [← map_negPolynomial, map_baseChange]

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