OAI/NumberTheory/Ostmann/Characters/HistoryUniqueness.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.Characters.frequencyDeterminant line 7
2. theorem OAI.Ostmann.Characters.reversal_determinant_dvd line 9
3. theorem OAI.Ostmann.Characters.reversal_determinant_zero line 17
4. theorem OAI.Ostmann.Characters.positive_coprime_denominator_unique line 28
5. theorem OAI.Ostmann.Characters.reversal_unique line 39