add_smul_of_equiv

Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point

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

← MathLib Explorer

English

For any P, add(P,P) equals dblXYZ(P).

Русский

Для любого P, add(P,P) = dblXYZ(P).

LaTeX

$$$\forall P : \mathrm{Fin}_3 \to R,\ \mathrm{add}(P,P) = \mathrm{dblXYZ}(P)$$$

Lean4

theorem add_smul_of_equiv {P Q : Fin 3 → R} (h : P ≈ Q) {u v : R} (hu : IsUnit u) (hv : IsUnit v) :
    W'.add (u • P) (v • Q) = u ^ 4 • W'.add P Q := by
  rw [add_of_equiv <| (smul_equiv_smul P Q hu hv).mpr h, dblXYZ_smul, add_of_equiv h]

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

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

Разделы

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

Аффилиация

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