Theorems · Inductive type · algebraic geometry
WeierstrassCurve.IsElliptic
{R : Type u} → [CommRing R] → WeierstrassCurve R → PropWeierstrassCurve.IsElliptic is a typeclass which asserts that a Weierstrass curve is an
elliptic curve: that its discriminant is a unit. Note that this definition is only mathematically
accurate for certain rings whose Picard group has trivial 12-torsion, such as a field or a PID.
- Cited by
- 52 results in Mathlib
- Foundations
- Depth 1 from the axioms · uses no axioms
- Assumes
- CommRing
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CommRingstatement · cited by 17,173
- WeierstrassCurvestatement · cited by 394
Cited by59
Results whose statement or proof uses this declaration.
- WeierstrassCurve.Δ'statement and proof · cited by 32
- WeierstrassCurve.jstatement and proof · cited by 27
- WeierstrassCurve.coe_Δ'statement and proof · cited by 11
- WeierstrassCurve.Affine.Point.mkstatement and proof · cited by 7
- WeierstrassCurve.Affine.pointEquivstatement and proof · cited by 4
- WeierstrassCurve.Affine.pointEquivSubtypestatement and proof · cited by 4
- WeierstrassCurve.j_eq_zero_iff'statement and proof · cited by 2
- WeierstrassCurve.j_eq_zero_iff_of_char_three'statement and proof · cited by 2
- WeierstrassCurve.j_eq_zero_iff_of_char_two'statement and proof · cited by 2
- WeierstrassCurve.map_Δ'statement and proof · cited by 2
- WeierstrassCurve.addSubMapCoeff_conditionstatement and proof · cited by 2
- WeierstrassCurve.inv_variableChange_Δ'statement and proof · cited by 1