Mathlib Map

Theorems · Theorem · algebraic geometry

WeierstrassCurve.Projective.nonsingular_neg

∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Projective F} {P : Fin 3 → F},
  W.Nonsingular P → W.Nonsingular (W.neg P)
Defined in
Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
Cited by
2 results in Mathlib
Foundations
Depth 116 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
Field
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

WeierstrassCurve.Projective.Point.toAffine_neg · cited by 1Point.toAffine_negWeierstrassCurve.Projective.nonsingularLift_negMap · cited by 0Projective.nonsingularLif…Field · cited by 7404FieldMatrix.vecCons · cited by 852Matrix.vecConsMatrix.vecEmpty · cited by 832Matrix.vecEmptyWeierstrassCurve.Projective · cited by 244WeierstrassCurve.Projecti…Ne.isUnit · cited by 99Ne.isUnitWeierstrassCurve.Affine.negY · cited by 56Affine.negYWeierstrassCurve.Projective.toAffine · cited by 47Projective.toAffineWeierstrassCurve.Projective.Nonsingular · cited by 37Projective.NonsingularIsUnit.neg · cited by 19IsUnit.negWeierstrassCurve.Projective.neg · cited by 18Projective.negWeierstrassCurve.Projective.isUnit_Y_of_Z_eq_zero · cited by 8Projective.isUnit_Y_of_Z_…WeierstrassCurve.Projective.nonsingular_smul · cited by 5Projective.nonsingular_sm…WeierstrassCurve.Projective.neg_of_Z_eq_zero · cited by 3Projective.neg_of_Z_eq_ze…WeierstrassCurve.Projective.neg_of_Z_ne_zero · cited by 3Projective.neg_of_Z_ne_ze…Projective.nonsingular_negCITED BYCITES

Cites14

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by2

Results whose statement or proof uses this declaration.