OAI/Combinatorics/Chromatic/QuantumTorus/WeakStrictUnitSelections.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.ElementaryPositivity.UnitSelections.Weak line 11
2. abbrev OAI.ElementaryPositivity.UnitSelections.Strict line 12
3. def OAI.ElementaryPositivity.UnitSelections.weakValues line 14
4. lemma OAI.ElementaryPositivity.UnitSelections.weakValues_injective line 17
5. lemma OAI.ElementaryPositivity.UnitSelections.weakValues_surjective line 27
6. def OAI.ElementaryPositivity.UnitSelections.weakSymEquiv line 40
7. lemma OAI.ElementaryPositivity.UnitSelections.strict_index_le line 43
8. def OAI.ElementaryPositivity.UnitSelections.staircaseEquiv line 55
9. lemma OAI.ElementaryPositivity.UnitSelections.staircase_sum line 79