Theorems · Theorem · algebraic geometry

WeierstrassCurve.Projective.map_equation

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

Defined in

Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic

Cited by

2 results in Mathlib

Foundations

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

Assumes

CommRingCommRing