baseChange_negAddY — Mathlib

English

Base change commutes with addXYZ: (W'.baseChange B).toJacobian.addXYZ (f ∘ P) = f ((W'.baseChange A).toJacobian.addXYZ P).

Русский

Базовое изменение commute с addXYZ: (W'.baseChange B).toJacobian.addXYZ (f ∘ P) = f ((W'.baseChange A).toJacobian.addXYZ P).

LaTeX

$$$ (W'.baseChange B).toJacobian.addXYZ (f \circ P) = f ((W'.baseChange A).toJacobian.addXYZ P) $$$

Lean4

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

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