map_neg

Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point

URI: https://scilib.ai/kg/mathlib#WeierstrassCurve.Jacobian.map_neg

← MathLib Explorer

English

A further consistency check for the additive equivalence under coordinate change.

Русский

Далее проверка согласованности эквиваленции сложения при смене координат.

LaTeX

$$proof3$$

Lean4

@[simp]
protected theorem map_neg (f : R →+* S) (P : Fin 3 → R) : (W'.map f).toJacobian.neg (f ∘ P) = f ∘ W'.neg P :=
  by
  simp only [neg, map_negY, comp_fin3]
  map_simp

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

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

Разделы

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

Аффилиация

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