OAI/Combinatorics/Progressions/Geometry/GradedTopCoordinates.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.NilpotentLieFiltration.quotientTopGradedMap_coordinate line 22
2. def OAI.Erdos3.NilpotentLieFiltration.quotientTopGradedSection line 39
3. theorem OAI.Erdos3.NilpotentLieFiltration.quotientTopGradedSection_basis line 42
4. theorem OAI.Erdos3.NilpotentLieFiltration.quotientTopGradedSection_coordinate line 46
5. theorem OAI.Erdos3.NilpotentLieFiltration.quotientTopGradedSection_coordinate_zero line 60
6. theorem OAI.Erdos3.NilpotentLieFiltration.quotientTopGradedSection_rightInverse line 73
7. theorem OAI.Erdos3.NilpotentLieFiltration.quotientTopGradedMap_kernel line 79
8. theorem OAI.Erdos3.NilpotentLieFiltration.reducedSquareGradedSndMap_coordinate line 95