map_negDblY — Mathlib

English

Let f: R → S be a ring hom and P: Fin 3 → R. Then the Y-coordinate of negated doubling on the mapped Jacobian equals the image under f of the original Y-coordinate, i.e., the construction negDblY is functorial with respect to f.

Русский

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

LaTeX

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

Lean4

@[simp]
theorem map_negDblY : (W'.map f).toJacobian.negDblY (f ∘ P) = f (W'.negDblY P) :=
  by
  simp only [negDblY, map_dblU, map_dblX, map_negY]
  simp

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