baseChange_negAddY — Mathlib

English

Let W′ be a Weierstrass projective curve over R. For P, Q : Fin 3 → A and f : A →ₛ B, the addX operation is compatible with base change (alternative naming):

Русский

Пусть W′ — проектная кривая Вейерштрасса над R. Для P, Q : Fin 3 → A и f : A →ₛ B операция addX сохраняется при базовом изменении (вариант названия):

LaTeX

$$$$(W'.baseChange B).toProjective.addX (f \circ P) (f \circ Q) = f \bigl((W'.baseChange A).toProjective.addX P Q\bigr)$$$$

Lean4

theorem baseChange_negAddY :
    (W'.baseChange B).toProjective.negAddY (f ∘ P) (f ∘ Q) = f ((W'.baseChange A).toProjective.negAddY P Q) := by
  rw [← RingHom.coe_coe, ← map_negAddY, map_baseChange]

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