Theorems · Theorem · algebraic geometry

WeierstrassCurve.Jacobian.Point.toAffine_of_Z_ne_zero

∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Jacobian F} {P : Fin 3 → F} (hP : W.Nonsingular P)
  (hPz : P 2 ≠ 0),
  WeierstrassCurve.Jacobian.Point.toAffine W P = WeierstrassCurve.Affine.Point.some (P 0 / P 2 ^ 2) (P 1 / P 2 ^ 3) ⋯

Defined in

Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point

Cited by

5 results in Mathlib

Foundations

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

Assumes

Field