Theorems · Theorem · algebraic geometry

WeierstrassCurve.Jacobian.map_add

∀ {F : Type u} {K : Type v} [inst : Field F] [inst_1 : Field K] {W : WeierstrassCurve.Jacobian F} (f : F →+* K)
  {P Q : Fin 3 → F}, W.Nonsingular P → W.Nonsingular Q → (W.map f).add (⇑f ∘ P) (⇑f ∘ Q) = ⇑f ∘ W.add P Q

Defined in

Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point

Cited by

1 results in Mathlib

Foundations

Depth 107 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FieldField