OAI/Combinatorics/Progressions/Linear/ComparisonChosenLayerBasis.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.Erdos3.RationalFilteredNilmanifold.MultidegreeStructure.SquarefreeBasisIndex line 18
2. def OAI.Erdos3.RationalFilteredNilmanifold.MultidegreeStructure.squarefreeBasis line 21
3. theorem OAI.Erdos3.RationalFilteredNilmanifold.MultidegreeStructure.squarefreeBasisIndex_card_le line 25
4. theorem OAI.Erdos3.RationalFilteredNilmanifold.MultidegreeStructure.squarefreeCoefficientBasis_card_le line 32
5. theorem OAI.Erdos3.RationalFilteredNilmanifold.MultidegreeStructure.squarefreeBasis_structure_height line 38
6. theorem OAI.Erdos3.RationalFilteredNilmanifold.MultidegreeStructure.squarefreeBasis_permute line 50
7. def OAI.Erdos3.RationalFilteredNilmanifold.MultidegreeStructure.comparisonLayerBasis line 72
8. theorem OAI.Erdos3.RationalFilteredNilmanifold.MultidegreeStructure.comparisonLayerBasis_height line 77