OAI/NumberTheory/Ostmann/Construction/DiagonalPermutationCountBasic.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.Ostmann.Construction.DiagonalPermutationCount.BulkPosition line 12
2. abbrev OAI.Ostmann.Construction.DiagonalPermutationCount.NonbulkPosition line 15
3. abbrev OAI.Ostmann.Construction.DiagonalPermutationCount.BandPermutation line 18
4. def OAI.Ostmann.Construction.DiagonalPermutationCount.bulkRestriction line 21
5. def OAI.Ostmann.Construction.DiagonalPermutationCount.nonbulkRestriction line 25
6. theorem OAI.Ostmann.Construction.DiagonalPermutationCount.restrictions_injective line 29
7. def OAI.Ostmann.Construction.DiagonalPermutationCount.orderedBulkRestriction line 42
8. theorem OAI.Ostmann.Construction.DiagonalPermutationCount.ordered_restrictions_injective line 47
9. theorem OAI.Ostmann.Construction.DiagonalPermutationCount.ordered_bulk_fiber_card_le line 62
10. theorem OAI.Ostmann.Construction.DiagonalPermutationCount.ordered_bulk_property_card_le line 76
11. theorem OAI.Ostmann.Construction.DiagonalPermutationCount.bad_arrangement_card_le line 94