Theorem IsEllipticSequence.normEDS

Modification history

2026-10-17 17:39
Mathlib/NumberTheory/EllipticDivisibilitySequence.lean
feat(NumberTheory/EllipticDivisibilitySequence): prove that a normalised elliptic divisibility sequence is an elliptic sequence (#42453) …
Added IsEllipticSequence.normEDSView on Github →