Theorems · Definition · number theory
preNormEDS
{R : Type u_1} → [CommRing R] → R → R → R → ℤ → RThe auxiliary sequence for a normalised EDS W : ℤ → R, with initial values
W(0) = 0, W(1) = 1, W(2) = 1, W(3) = c, and W(4) = d and extra parameter b.
This extends preNormEDS' by defining its values at negative integers.
- Cited by
- 25 results in Mathlib
- Foundations
- Depth 71 from the axioms · uses propext, Classical.choice, Quot.sound
- 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 and proof · cited by 17,173
- preNormEDS'proof · cited by 15
Cited by28
Results whose statement or proof uses this declaration.
- WeierstrassCurve.preΨproof · cited by 33
- normEDSproof · cited by 18
- complEDS₂proof · cited by 16
- preNormEDS_onestatement · cited by 8
- preNormEDS_twostatement · cited by 8
- preNormEDS_negstatement · cited by 7
- preNormEDS_threestatement · cited by 7
- preNormEDS_zerostatement · cited by 6
- preNormEDS_fourstatement · cited by 5
- preNormEDS_ofNatstatement · cited by 4
- map_preNormEDSstatement · cited by 4
- WeierstrassCurve.map_preΨproof · cited by 4