OAI/Combinatorics/Progressions/Dynamics/RealProjectedPotentialGroupIdentity.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.PolynomialTranslationLie.continuous_pair_pullback line 17
2. theorem OAI.Erdos3.PolynomialTranslationLie.continuous_pair_potential_difference line 24
3. theorem OAI.Erdos3.PolynomialTranslationLie.realification_pair_eq_of_rational line 33
4. theorem OAI.Erdos3.PolynomialTranslationLie.eval_real_map_at_rational line 53
5. theorem OAI.Erdos3.PolynomialTranslationLie.bchRealTranslationHom_rational_eval_potential line 59
6. theorem OAI.Erdos3.PolynomialTranslationLie.bchRealTranslationHom_eval_potential_on_real_base_image line 94
7. theorem OAI.Erdos3.PolynomialTranslationLie.bchRealTranslationHom_eval_potential line 147