baseChange_addY — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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