Theorems · Definition · number theory

normEDS

{R : Type u_1} → [CommRing R] → R → R → R → ℤ → R

The canonical example of a normalised EDS W : ℤ → R, with initial values W(0) = 0, W(1) = 1, W(2) = b, W(3) = c, and W(4) = d * b. This is defined in terms of preNormEDS whose even terms differ by a factor of b.

Defined in

Mathlib.NumberTheory.EllipticDivisibilitySequence

Cited by

18 results in Mathlib

Foundations

Depth 72 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRing