Mathlib Map

Theorems · Theorem · number theory

normEDS_odd

∀ {R : Type u_1} [inst : CommRing R] (b c d : R) (m : ℤ),
  normEDS b c d (2 * m + 1) =
    normEDS b c d (m + 2) * normEDS b c d m ^ 3 - normEDS b c d (m - 1) * normEDS b c d (m + 1) ^ 3
Defined in
Mathlib.NumberTheory.EllipticDivisibilitySequence
Cited by
1 results in Mathlib
Foundations
Depth 75 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
CommRing
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

WeierstrassCurve.ψ_odd · cited by 1WeierstrassCurve.ψ_oddCommRing · cited by 17173CommRingNat.cast_one · cited by 2501Nat.cast_oneEven · cited by 444EvenpreNormEDS · cited by 25preNormEDSnormEDS · cited by 18normEDSInt.not_even_two_mul_add_one · cited by 3Int.not_even_two_mul_add_…preNormEDS_odd · cited by 2preNormEDS_oddnormEDS_oddCITED BYCITES

Cites7

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

Cited by1

Results whose statement or proof uses this declaration.