OAI/Combinatorics/Progressions/Estimates/SquarefreeLayerBases.lean
6 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.Erdos3.MultidegreeLieFiltration.squarefreeSupportedFinBasisline 17 - theorem
OAI.Erdos3.MultidegreeLieFiltration.squarefreeSupportedFinBasis_heightline 25 - def
OAI.Erdos3.MultidegreeLieFiltration.squarefreeMultidegreeBasisline 32 - theorem
OAI.Erdos3.MultidegreeLieFiltration.squarefreeMultidegreeBasis_heightline 36 - def
OAI.Erdos3.MultidegreeLieFiltration.squarefreeDegreeBasisline 40 - theorem
OAI.Erdos3.MultidegreeLieFiltration.squarefreeDegreeBasis_heightline 44