OAI/Combinatorics/Chromatic/Walls/FiltrationHomogeneousRank.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ElementaryPositivity.LinearFiltration.homogeneousMk line 13
2. lemma OAI.ElementaryPositivity.LinearFiltration.homogeneousMk_range line 20
3. lemma OAI.ElementaryPositivity.LinearFiltration.homogeneousMap_finite line 35
4. lemma OAI.ElementaryPositivity.LinearFiltration.homogeneousMk_ker line 40
5. lemma OAI.ElementaryPositivity.LinearFiltration.homogeneousGrade_rank line 48
6. lemma OAI.ElementaryPositivity.LinearFiltration.homogeneousGrade_rank_eq line 59
7. lemma OAI.ElementaryPositivity.finiteFiltration_rank_step line 80
8. lemma OAI.ElementaryPositivity.finiteFiltration_rank_sum line 87
9. lemma OAI.ElementaryPositivity.finiteFiltration_rank_total line 99