Theorem IsEllipticNet.atom_mul_atomRel

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