Theorem normEDS_rel_odd

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 normEDS_rel_oddView on Github →