Theorem IsEllipticSequence.of_even_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 IsEllipticSequence.of_even_oddView on Github →