Theorem IsEllipticNet.atomRel_perm

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 IsEllipticNet.atomRel_permView on Github →