baseChange_dblXYZ — Mathlib

English

Under base change, the negAddY coordinate commutes with f: (W'.baseChange B).toJacobian.negAddY (f ∘ P) = f ((W'.baseChange A).toJacobian.negAddY P).

Русский

При базовом изменении координата negAddY совместима с отображением: (W'.baseChange B).toJacobian.negAddY (f ∘ P) = f ((W'.baseChange A).toJacobian.negAddY P).

LaTeX

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

Lean4

theorem baseChange_dblXYZ : (W'.baseChange B).toJacobian.dblXYZ (f ∘ P) = f ∘ (W'.baseChange A).toJacobian.dblXYZ P :=
  by rw [← RingHom.coe_coe, ← map_dblXYZ, map_baseChange]

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