OAI/Combinatorics/Chromatic/QuantumTorus/WeakUnitRecursion.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ElementaryPositivity.UnitSelections.prependZero line 11
2. def OAI.ElementaryPositivity.UnitSelections.deleteZeroEquiv line 19
3. lemma OAI.ElementaryPositivity.UnitSelections.weak_first_le line 30
4. def OAI.ElementaryPositivity.UnitSelections.shiftOne line 33
5. def OAI.ElementaryPositivity.UnitSelections.subtractOneEquiv line 36
6. def OAI.ElementaryPositivity.UnitSelections.weakSplit line 53
7. lemma OAI.ElementaryPositivity.UnitSelections.weight_prependZero line 57
8. lemma OAI.ElementaryPositivity.UnitSelections.weight_shiftOne line 62
9. lemma OAI.ElementaryPositivity.UnitSelections.weakSplit_inv_energy line 65