OAI/Combinatorics/Chromatic/QuantumTorus/UnitRowSelection.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ElementaryPositivity.UnitSelections.unitSigmaSubtype line 12
2. lemma OAI.ElementaryPositivity.UnitSelections.ofFn_signed_iff line 19
3. def OAI.ElementaryPositivity.UnitSelections.unitWordEquiv line 40
4. def OAI.ElementaryPositivity.UnitSelections.unitRowSelection line 44
5. def OAI.ElementaryPositivity.UnitSelections.unitRowCount line 47
6. lemma OAI.ElementaryPositivity.UnitSelections.unitRowSelection_val line 50
7. lemma OAI.ElementaryPositivity.UnitSelections.unitRowSelection_card line 53
8. lemma OAI.ElementaryPositivity.UnitSelections.unitRowSelection_energy line 57
9. lemma OAI.ElementaryPositivity.UnitSelections.multiset_count_energy line 70
10. lemma OAI.ElementaryPositivity.UnitSelections.unitRowCount_energy line 82
11. abbrev OAI.ElementaryPositivity.UnitSelections.ColumnSelection line 91
12. def OAI.ElementaryPositivity.UnitSelections.columnRowEquiv line 93
13. def OAI.ElementaryPositivity.UnitSelections.unitRowsEquiv line 99
14. lemma OAI.ElementaryPositivity.UnitSelections.unitRows_split line 103
15. lemma OAI.ElementaryPositivity.UnitSelections.sigma_sum_univ line 110
16. lemma OAI.ElementaryPositivity.UnitSelections.unitRows_energy line 121