OAI/Combinatorics/Progressions/Estimates/FormalExpLog.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.formalSeries_eq_of_derivative_eq line 12
2. theorem OAI.Erdos3.formal_log_derivative_mul line 23
3. theorem OAI.Erdos3.formal_log_derivative_subst line 33
4. theorem OAI.Erdos3.formal_log_exp line 38
5. theorem OAI.Erdos3.formal_exp_sub_one_log line 49
6. theorem OAI.Erdos3.formal_exp_log line 54