OAI/Combinatorics/Progressions/Polynomial/PolynomialTranslationIntegralAction.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos3.PolynomialTranslationGroup.fromInteger line 12
2. theorem OAI.Erdos3.PolynomialTranslationGroup.fromInteger_base line 17
3. theorem OAI.Erdos3.PolynomialTranslationGroup.fromInteger_polynomial line 20
4. def OAI.Erdos3.PolynomialTranslationGroup.integralGroup line 23
5. theorem OAI.Erdos3.PolynomialTranslationGroup.mem_integralGroup_iff line 25
6. theorem OAI.Erdos3.PolynomialTranslationGroup.integralGroup_action_integral line 38
7. theorem OAI.Erdos3.PolynomialTranslationGroup.mem_integralGroup_iff_action line 48
8. theorem OAI.Erdos3.PolynomialTranslationGroup.mem_integralGroup_iff_action_and_inverse line 69
9. theorem OAI.Erdos3.PolynomialTranslationLie.bchTranslationHom_mem_integralGroup_iff line 88
10. theorem OAI.Erdos3.PolynomialTranslationLie.bchTranslation_integral_comap line 96