Theorems · Definition · algebraic geometry

WeierstrassCurve.Jacobian.Point.noConfusion

{P : Sort u} →
  {R : Type r} →
    {inst : CommRing R} →
      {W' : WeierstrassCurve.Jacobian R} →
        {t : W'.Point} →
          {R' : Type r} →
            {inst' : CommRing R'} →
              {W'' : WeierstrassCurve.Jacobian R'} →
                {t' : W''.Point} →
                  R = R' → inst ≍ inst' → W' ≍ W'' → t ≍ t' → WeierstrassCurve.Jacobian.Point.noConfusionType P t t'

Defined in

Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point

Cited by

0 results in Mathlib

Foundations

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