OAI/NumberTheory/Ostmann/Construction/ScheduledAmplitudeAlphabet.lean
1 declarations, 0 contain sorry, 0 declared as axioms
The scheduled initial weight restricts to its actual regular-prime alphabet
- theorem
OAI.Ostmann.scheduledCellAmplitude_initial_prime_alphabetline 11