Theorems · Theorem · algebraic geometry

WeierstrassCurve.Affine.nonsingularPointEquivSubtype_symm_some

∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Affine R} {x y : R} {h : W'.Nonsingular x y}
  {p : W'.Point → Prop} (p0 : p WeierstrassCurve.Affine.Point.zero) (ph : p (WeierstrassCurve.Affine.Point.some x y h)),
  (WeierstrassCurve.Affine.nonsingularPointEquivSubtype p0).symm (some ⟨(x, y), ⋯⟩) =
    ⟨WeierstrassCurve.Affine.Point.some x y h, ph⟩

Defined in

Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommRing