baseChange_dblX — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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