OAI/Combinatorics/Progressions/Dynamics/ActualPathCurrentGradeReset.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.exists_actual_path_reset_budget line 9
2. theorem OAI.Erdos3.NilpotentLieFiltration.symbolPointwiseSubalgebra_basisGraded line 49
3. theorem OAI.Erdos3.NilpotentLieFiltration.exists_restricted_path_common_quotient_splitting line 63
4. theorem OAI.Erdos3.NilpotentLieFiltration.exists_symbol_reset_from_restricted_path line 97
5. theorem OAI.Erdos3.NilpotentLieFiltration.exists_actual_path_common_quotient_splitting line 165
6. theorem OAI.Erdos3.NilpotentLieFiltration.exists_actual_path_current_grade_reset line 207