map_addY

Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula

URI: https://scilib.ai/kg/mathlib#WeierstrassCurve.Projective.map_addY

← MathLib Explorer

English

The neg-addY map respects ring homomorphisms: map_negAddY (W', f) (P,Q) = f(negAddY P Q).

Русский

Отображение negAddY сохраняется под f.

LaTeX

$$$$(W'.map f).toProjective.negAddY (f\circ P) (f\circ Q) = f(W'.negAddY P Q)$$$$

Lean4

@[simp]
theorem map_addY : (W'.map f).toProjective.addY (f ∘ P) (f ∘ Q) = f (W'.addY P Q) :=
  by
  simp only [addY, negY_eq, map_negAddY, map_addX, map_addZ]
  map_simp

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru