OAI/Combinatorics/Progressions/Estimates/SimultaneousSymbolSplitting.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.NilpotentLieFiltration.symbolSlowBound_one line 16
2. theorem OAI.Erdos3.NilpotentLieFiltration.symbolRationalGrid_one line 23
3. theorem OAI.Erdos3.NilpotentLieFiltration.realSymbolGradeQuotientHom_first line 32
4. theorem OAI.Erdos3.NilpotentLieFiltration.realSymbolGradeQuotient_mem_terminal_iff line 40
5. theorem OAI.Erdos3.NilpotentLieFiltration.exists_controlled_terminal_symbol_comparison line 60
6. theorem OAI.Erdos3.NilpotentLieFiltration.exists_simultaneous_symbol_extension line 107
7. theorem OAI.Erdos3.NilpotentLieFiltration.exists_simultaneous_symbol_splitting line 287