Structures · Geometry
WeierstrassCurve.IsElliptic
WeierstrassCurve.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.
- Shape
- One type argument · adds isUnit
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances0
No instance on a concrete type; it is reached through other classes.
How is a type an instance?
Loading the hierarchy index…
Assumed by55
- WeierstrassCurve.Δ'
- WeierstrassCurve.j
- WeierstrassCurve.coe_Δ'
- WeierstrassCurve.Affine.pointEquivSubtype
- WeierstrassCurve.Affine.pointEquiv
- WeierstrassCurve.j_eq_zero_iff'
- WeierstrassCurve.j_eq_zero_iff_of_char_three'
- WeierstrassCurve.j_eq_zero_iff_of_char_two'
- WeierstrassCurve.addSubMapCoeff_condition
- WeierstrassCurve.map_Δ'
- WeierstrassCurve.j_of_isCharThreeJNeZeroNF_of_char_three
- WeierstrassCurve.coe_inv_map_Δ'
- WeierstrassCurve.j.congr_simp
- WeierstrassCurve.coe_map_Δ'
- WeierstrassCurve.j_of_char_two
- WeierstrassCurve.j_of_char_three
- WeierstrassCurve.IsElliptic.isUnit
- WeierstrassCurve.coe_inv_variableChange_Δ'
- WeierstrassCurve.inv_variableChange_Δ'
- WeierstrassCurve.variableChange_Δ'
- WeierstrassCurve.j_of_isCharTwoJNeZeroNF_of_char_two
- WeierstrassCurve.isUnit_Δ
- WeierstrassCurve.j_eq_zero_of_char_two
- WeierstrassCurve.j_eq_zero
- WeierstrassCurve.j_of_isCharTwoJEqZeroNF
- WeierstrassCurve.Δ'.congr_simp
- WeierstrassCurve.j_ne_zero_of_isCharThreeJNeZeroNF_of_char_three
- WeierstrassCurve.addSubMap_ne_zero
- WeierstrassCurve.j_ne_zero_of_isCharTwoJNeZeroNF_of_char_two
- WeierstrassCurve.twoTorsionPolynomial_discr_ne_zero_of_isElliptic
- WeierstrassCurve.inv_map_Δ'
- WeierstrassCurve.Affine.pointEquiv_some
- WeierstrassCurve.exists_variableChange_of_j_eq
- WeierstrassCurve.j_eq_zero_of_char_three
- WeierstrassCurve.j_of_isShortNF_of_char_three
- WeierstrassCurve.instIsEllipticHSMulVariableChange
- WeierstrassCurve.map_j
- WeierstrassCurve.Affine.equation_iff_nonsingular
- WeierstrassCurve.j_eq_zero_iff_of_char_three
- WeierstrassCurve.abs_logHeight_addSubMap_sub_two_mul_logHeight_le
- WeierstrassCurve.Affine.pointEquivSubtype_some
- WeierstrassCurve.instIsEllipticMap
- WeierstrassCurve.Affine.pointEquiv_zero
- WeierstrassCurve.Affine.pointEquivSubtype_zero
- WeierstrassCurve.j_of_isCharTwoJEqZeroNF_of_char_two
- WeierstrassCurve.Affine.pointEquiv_symm_none
- WeierstrassCurve.j_eq_zero_iff
- WeierstrassCurve.Affine.pointEquivSubtype_symm_none
- WeierstrassCurve.j_eq_zero_iff_of_char_two
- WeierstrassCurve.variableChange_j
Ancestors0
No ancestors.