Theorems · Theorem · algebraic geometry

WeierstrassCurve.map_variableChange

∀ {R : Type u} [inst : CommRing R] (W : WeierstrassCurve R) (C : WeierstrassCurve.VariableChange R) {A : Type v}
  [inst_1 : CommRing A] (φ : R →+* A), C.map φ • W.map φ = (C • W).map φ

Defined in

Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommRingCommRing