OAI/Combinatorics/Progressions/Linear/HomogeneousLieSpan.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos3.homogeneousLieSpan line 14
2. theorem OAI.Erdos3.homogeneousLieSpan_mono line 17
3. theorem OAI.Erdos3.homogeneousLieSpan_empty line 23
4. structure OAI.Erdos3.LieGradingExpansion line 27
5. def OAI.Erdos3.LieGradingExpansion.component line 36
6. theorem OAI.Erdos3.LieGradingExpansion.component_apply line 39
7. theorem OAI.Erdos3.LieGradingExpansion.component_tree line 42
8. theorem OAI.Erdos3.LieGradingExpansion.component_mem_span line 49
9. theorem OAI.Erdos3.LieGradingExpansion.component_eq_zero line 63
10. theorem OAI.Erdos3.LieGradingExpansion.span_inter line 74