Mathlib Map

Theorems · Theorem · number theory

normEDS_even

∀ {R : Type u_1} [inst : CommRing R] (b c d : R) (m : ℤ),
  normEDS b c d (2 * m) * b =
    normEDS b c d (m - 1) ^ 2 * normEDS b c d m * normEDS b c d (m + 2) -
      normEDS b c d (m - 2) * normEDS b c d m * normEDS b c d (m + 1) ^ 2
Defined in
Mathlib.NumberTheory.EllipticDivisibilitySequence
Cited by
1 results in Mathlib
Foundations
Depth 77 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.ψ_even · cited by 0WeierstrassCurve.ψ_evenCommRing · cited by 17173CommRingmul_assoc · cited by 1667mul_assocnormEDS · cited by 18normEDScomplEDS₂ · cited by 16complEDS₂normEDS_mul_complEDS₂ · cited by 2normEDS_mul_complEDS₂complEDS₂_mul_b · cited by 1complEDS₂_mul_bnormEDS_evenCITED BYCITES

Cites6

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.