addMap — Mathlib

English

The map on quotient representatives behaves compatibly with the addition on the Jacobian: addMap of representatives equals the representative of the sum.

Русский

Отображение addMap на представители в фактор-множество совместимо с операцией сложения на Якобиане: addMap представителя равен представителю суммы.

LaTeX

$$$W'.addMap\,\overline{P}\,\overline{Q} = \overline{W'.add(P,Q)}$$$

Lean4

/-- The addition of two Jacobian point classes on a Weierstrass curve `W`.

If `P` and `Q` are two Jacobian point representatives on `W`, then `W.addMap ⟦P⟧ ⟦Q⟧` is
definitionally equivalent to `W.add P Q`. -/
noncomputable def addMap (P Q : PointClass R) : PointClass R :=
  Quotient.map₂ W'.add (fun _ _ hP _ _ hQ => add_equiv hP hQ) P Q

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