OAI/NumberTheory/Ostmann/Arithmetic/PermutationHaarConvention.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.Arithmetic.PermutationHaarConvention.rowConjugate line 12
2. theorem OAI.Ostmann.Arithmetic.PermutationHaarConvention.overlapRelation_rowConjugate line 17
3. theorem OAI.Ostmann.Arithmetic.PermutationHaarConvention.eqvGen_map line 23
4. theorem OAI.Ostmann.Arithmetic.PermutationHaarConvention.overlapClosure_rowConjugate line 32
5. def OAI.Ostmann.Arithmetic.PermutationHaarConvention.rowComponentEquiv line 44
6. theorem OAI.Ostmann.Arithmetic.PermutationHaarConvention.overlapComponent_card_rowConjugate line 49
7. theorem OAI.Ostmann.Arithmetic.PermutationHaarConvention.haarPermutation_blocks line 54
8. theorem OAI.Ostmann.Arithmetic.PermutationHaarConvention.haarPermutation_badArrangement_iff line 61
9. theorem OAI.Ostmann.Arithmetic.PermutationHaarConvention.haarPermutation_transferBadArrangement_iff line 68
10. theorem OAI.Ostmann.Arithmetic.PermutationHaarConvention.haarPermutation_good line 73