map_dblXYZ

Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula

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

← MathLib Explorer

English

The addition-by-U map commutes with ring homomorphisms: map_addU(f)(P,Q) = f(addU(P,Q)).

Русский

Сложение по U сохраняется под отображением: map_addU(f)(P,Q) = f(addU(P,Q)).

LaTeX

$$$\mathrm{addU}(f\circ P, f\circ Q) = f(\mathrm{addU}(P,Q))$$$

Lean4

@[simp]
theorem map_dblXYZ : (W'.map f).toProjective.dblXYZ (f ∘ P) = f ∘ dblXYZ W' P := by
  simp only [dblXYZ, map_dblX, map_dblY, map_dblZ, comp_fin3]

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

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

Разделы

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

Аффилиация

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