baseChange_dblZ — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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