map_dblY — Mathlib

English

Let f: R → S be a ring hom and P: Fin 3 → R. The Y-coordinate of the mapped Jacobian under f commutes with f on the original Y-coordinate: (W'.map f).toJacobian.dblY (f ∘ P) = f (W'.dblY P).

Русский

Пусть f: R → S — кольцевой гомоморфизм и P: Fin 3 → R. Тогда dblY естественно претерпевает отображение: (W'.map f).toJacobian.dblY (f ∘ P) = f (W'.dblY P).

LaTeX

$$$ (W'.map f).toJacobian.dblY (f \circ P) = f (W'.dblY P) $$$

Lean4

@[simp]
theorem map_dblY : (W'.map f).toJacobian.dblY (f ∘ P) = f (W'.dblY P) :=
  by
  simp only [dblY, negY_eq, map_negDblY, map_dblX, map_dblZ]
  map_simp

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