Theorems · Theorem · algebraic geometry

WeierstrassCurve.Affine.Point.map_baseChange

∀ {R : Type r} {F : Type u} {K : Type v} {L : Type w} [inst : CommRing R] [inst_1 : Field F] [inst_2 : Field K]
  [inst_3 : Field L] {W' : WeierstrassCurve.Affine R} [inst_4 : DecidableEq F] [inst_5 : DecidableEq K]
  [inst_6 : DecidableEq L] [inst_7 : Algebra R F] [inst_8 : Algebra R K] [inst_9 : Algebra R L] [inst_10 : Algebra F K]
  [inst_11 : IsScalarTower R F K] [inst_12 : Algebra F L] [inst_13 : IsScalarTower R F L] (f : K →ₐ[F] L)
  (P : (W'.baseChange F).Point),
  (WeierstrassCurve.Affine.Point.map f) ((WeierstrassCurve.Affine.Point.baseChange F K) P) =
    (WeierstrassCurve.Affine.Point.baseChange F L) P

Defined in

Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommRingFieldFieldFieldDecidableEqDecidableEqDecidableEqAlgebraAlgebraAlgebraAlgebraIsScalarTowerAlgebraIsScalarTower