Theorems · Theorem · number theory
preNormEDS_even
∀ {R : Type u_1} [inst : CommRing R] (b c d : R) (m : ℤ),
preNormEDS b c d (2 * m) =
preNormEDS b c d (m - 1) ^ 2 * preNormEDS b c d m * preNormEDS b c d (m + 2) -
preNormEDS b c d (m - 2) * preNormEDS b c d m * preNormEDS b c d (m + 1) ^ 2- Cited by
- 2 results in Mathlib
- Foundations
- Depth 74 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.
Cites27
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
- mul_oneproof · cited by 3,885
- one_mulproof · cited by 2,841
- Nat.cast_oneproof · cited by 2,501
- zero_addproof · cited by 2,366
- MulZeroClass.mul_zeroproof · cited by 2,091
- Nat.cast_zeroproof · cited by 1,870
- MulZeroClass.zero_mulproof · cited by 1,625
- sub_selfproof · cited by 996
- sub_zeroproof · cited by 938
- mul_negproof · cited by 590
- one_powproof · cited by 521
Cited by2
Results whose statement or proof uses this declaration.
- WeierstrassCurve.preΨ_evenproof · cited by 2
- preNormEDS_mul_complEDS₂proof · cited by 1