Theorems · Theorem · algebraic geometry

WeierstrassCurve.Affine.Point.map_some

∀ {R : Type r} {S : Type s} {F : Type u} {K : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Field F]
  [inst_3 : Field K] {W' : WeierstrassCurve.Affine R} [inst_4 : DecidableEq F] [inst_5 : DecidableEq K]
  [inst_6 : Algebra R S] [inst_7 : Algebra R F] [inst_8 : Algebra S F] [inst_9 : IsScalarTower R S F]
  [inst_10 : Algebra R K] [inst_11 : Algebra S K] [inst_12 : IsScalarTower R S K] (f : F →ₐ[S] K) {x y : F}
  (h : (W'.baseChange F).Nonsingular x y),
  (WeierstrassCurve.Affine.Point.map f) (WeierstrassCurve.Affine.Point.some x y h) =
    WeierstrassCurve.Affine.Point.some (f x) (f y) ⋯

Defined in

Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommRingCommRingFieldFieldDecidableEqDecidableEqAlgebraAlgebraAlgebraIsScalarTowerAlgebraAlgebraIsScalarTower