Theorem normEDS'_one

Modification history

2024-05-16 07:16

Mathlib/NumberTheory/EllipticDivisibilitySequence.lean

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

Deleted normEDS'_one View on Github →

2024-01-22 20:12

Mathlib/NumberTheory/EllipticDivisibilitySequence.lean

feat(NumberTheory/EllipticDivisibilitySequence): define elliptic divisibility sequences (#9375) …

Added normEDS'_one View on Github →