Theorems · Theorem · algebraic geometry

WeierstrassCurve.Jacobian.map_nonsingular

∀ {R : Type r} [inst : CommRing R] (W' : WeierstrassCurve.Jacobian R) {S : Type s} [inst_1 : CommRing S] {f : R →+* S},
  Function.Injective ⇑f → ∀ (P : Fin 3 → R), (W'.map f).Nonsingular (⇑f ∘ P) ↔ W'.Nonsingular P

Defined in

Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRingCommRing