OAI/NumberTheory/OrdinaryCorrelations/AbsoluteDefect/CharBounded.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.OrdinaryCorrelations.ResidueCharacters.char_bounded line 27
2. lemma OAI.OrdinaryCorrelations.ResidueCharacters.char_multiplicative line 30
3. lemma OAI.OrdinaryCorrelations.ResidueCharacters.char_one line 35
4. lemma OAI.OrdinaryCorrelations.ResidueCharacters.char_inv_eq_star line 37
5. theorem OAI.OrdinaryCorrelations.ResidueCharacters.unit_indicator line 43
6. theorem OAI.OrdinaryCorrelations.ResidueCharacters.dilated_indicator line 58
7. theorem OAI.OrdinaryCorrelations.ResidueCharacters.gcd_indicator line 74