OAI/Combinatorics/Progressions/Polynomial/SquarefreeTopDegree.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos3.SquarefreeIndex.full line 9
2. theorem OAI.Erdos3.SquarefreeIndex.full_apply line 12
3. theorem OAI.Erdos3.SquarefreeIndex.one_le_iff line 15
4. theorem OAI.Erdos3.SquarefreeIndex.permute_full line 26
5. theorem OAI.Erdos3.squarefree_top_monomial line 32
6. theorem OAI.Erdos3.MultidegreeLieFiltration.squarefreeBlockPermute_eq_self_top line 50