Theorems · Definition · algebraic geometry

WeierstrassCurve.Projective.map

{R : Type r} →
  [inst : CommRing R] →
    WeierstrassCurve.Projective R → {S : Type s} → [inst_1 : CommRing S] → (R →+* S) → WeierstrassCurve.Projective S

The Weierstrass curve in projective coordinates mapped over a ring homomorphism f : R →+* S.

Defined in

Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic

Cited by

25 results in Mathlib

Foundations

Depth 17 from the axioms · uses no axioms

Assumes

CommRingCommRing