OAI/Combinatorics/Progressions/Estimates/RestrictedGradeMajorMatching.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos3.NilpotentLieFiltration.RestrictedMajorGradeCorrectionConclusion line 13
2. def OAI.Erdos3.NilpotentLieFiltration.RestrictedDetectedMajorGradeConclusion line 63
3. theorem OAI.Erdos3.NilpotentLieFiltration.restrictedDetectedMajorGradeConclusion_of_vector_detection line 83
4. theorem OAI.Erdos3.NilpotentLieFiltration.exists_restricted_grade_scalar_major_detections line 130
5. theorem OAI.Erdos3.NilpotentLieFiltration.exists_restricted_grade_vector_major_detection line 199
6. theorem OAI.Erdos3.NilpotentLieFiltration.exists_restricted_grade_major_matching line 266