OAI/Combinatorics/Chromatic/GradedAlgebra/CompleteUnit.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ElementaryPositivity.UnitSelections.laurent_q_not_root line 14
2. theorem OAI.ElementaryPositivity.UnitSelections.weakSeries_eq_complete line 21
3. theorem OAI.ElementaryPositivity.UnitSelections.complete_literal_expansion line 29
4. def OAI.ElementaryPositivity.UnitSelections.strictEnergy line 41
5. lemma OAI.ElementaryPositivity.UnitSelections.strictAdmissible line 43
6. def OAI.ElementaryPositivity.UnitSelections.strictSeries line 57
7. lemma OAI.ElementaryPositivity.UnitSelections.strictSeries_staircase line 59
8. lemma OAI.ElementaryPositivity.UnitSelections.twice_range_staircase line 69
9. theorem OAI.ElementaryPositivity.UnitSelections.elementary_literal_expansion line 75
10. lemma OAI.ElementaryPositivity.EnergyLaurent.admissible_equiv line 92
11. def OAI.ElementaryPositivity.EnergyLaurent.finSuccPi line 104
12. lemma OAI.ElementaryPositivity.EnergyLaurent.admissible_fin_pi line 111
13. lemma OAI.ElementaryPositivity.EnergyLaurent.series_fin_pi line 125