OAI/NumberTheory/Ostmann/Characters/HigherBiasSourceCellSumsDensity.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Ostmann.Characters.NormalizedCellSet.affine_injective line 10
2. lemma OAI.Ostmann.Characters.NormalizedCellSet.card_eq line 15
3. lemma OAI.Ostmann.Characters.NormalizedCellSet.card_le_endpoint line 20
4. lemma OAI.Ostmann.Characters.NormalizedCellSet.card_le_residue_card_add_one line 27
5. theorem OAI.Ostmann.Characters.NormalizedCellSet.real_margins line 46
6. lemma OAI.Ostmann.Characters.NormalizedCellSet.residue_generates line 67