OAI/Combinatorics/Progressions/Dynamics/ProjectedPotentialGroupIdentity.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos3.PolynomialTranslationLie.projectedSubalgebra line 13
2. theorem OAI.Erdos3.PolynomialTranslationLie.projected_pure_constant_zero line 18
3. def OAI.Erdos3.PolynomialTranslationLie.projectedPotentialRelation line 44
4. theorem OAI.Erdos3.PolynomialTranslationLie.projectedSubalgebra_base_surjective line 60
5. theorem OAI.Erdos3.PolynomialTranslationLie.exists_potential_on_projected_base line 75
6. def OAI.Erdos3.PolynomialTranslationLie.projectedFastGenerators line 114
7. theorem OAI.Erdos3.PolynomialTranslationLie.projectedFastGenerators_mem_potential line 121
8. theorem OAI.Erdos3.PolynomialTranslationLie.projectedFastSubgroup_potential_identity line 136
9. theorem OAI.Erdos3.PolynomialTranslationLie.eval_polynomialTranslate line 156
10. theorem OAI.Erdos3.PolynomialTranslationLie.projectedFastSubgroup_eval_potential_identity line 163