Theorem preNormEDS'_one

Modification history

2024-05-17 06:05

Mathlib/NumberTheory/EllipticDivisibilitySequence.lean

chore(EllipticDivisibilitySequence): backport change for nightly-testing (#12969) …

Modified preNormEDS'_one View on Github →

2024-05-16 07:16

Mathlib/NumberTheory/EllipticDivisibilitySequence.lean

feat(NumberTheory/EllipticDivisibilitySequence): expose the auxiliary sequence (#10814) …

Added preNormEDS'_one View on Github →