Theorems · Theorem · algebraic geometry

WeierstrassCurve.Jacobian.Point.toAffine_add

∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Jacobian F} [inst_1 : DecidableEq F] {P Q : Fin 3 → F},
  W.Nonsingular P →
    W.Nonsingular Q →
      WeierstrassCurve.Jacobian.Point.toAffine W (W.add P Q) =
        WeierstrassCurve.Jacobian.Point.toAffine W P + WeierstrassCurve.Jacobian.Point.toAffine W Q

Defined in

Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point

Cited by

1 results in Mathlib

Foundations

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

Assumes

FieldDecidableEq