OAI/Combinatorics/Progressions/Nilpotent/RankBracketFactorizationMonotone.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.NilpotentLieFiltration.refiltered_lieTreeEval_mem line 15
2. theorem OAI.Erdos3.RationalFilteredNilmanifold.DegreeRankStructure.refiltered_rank_bracket_frequency line 31
3. theorem OAI.Erdos3.realifyFunctional_sub_apply line 65
4. theorem OAI.Erdos3.realifyFunctional_eq_on_submodule line 74
5. theorem OAI.Erdos3.NilpotentLieFiltration.real_refiltered_lieTreeEval_mem line 91
6. theorem OAI.Erdos3.RationalFilteredNilmanifold.DegreeRankStructure.real_refiltered_rank_bracket_frequency line 107
7. def OAI.Erdos3.RationalFilteredNilmanifold.DegreeRankStructure.ControlledRankBracketFactorization line 148
8. theorem OAI.Erdos3.RationalFilteredNilmanifold.DegreeRankStructure.controlledRankBracketFactorization_of_frequency_restriction line 167
9. theorem OAI.Erdos3.RationalFilteredNilmanifold.DegreeRankStructure.ControlledRankBracketFactorization.exists_in line 195
10. theorem OAI.Erdos3.RationalFilteredNilmanifold.DegreeRankStructure.ControlledRankBracketFactorization.mono line 224