OAI/NumberTheory/PiExponent/Analysis/LogarithmicObstruction.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PiExponent.laurent_derivative_residue_eq_zero line 15
2. theorem OAI.PiExponent.laurent_derivative_ne_simple_pole line 19
3. theorem OAI.PiExponent.polynomial_logarithmic_equation_impossible line 28
4. theorem OAI.PiExponent.ratFunc_derivation_polynomial line 68
5. theorem OAI.PiExponent.ratFunc_derivation_ne_simple_pole line 75
6. theorem OAI.PiExponent.derivation_intermediate_smul line 101
7. theorem OAI.PiExponent.derivation_basis_coordinates line 111
8. theorem OAI.PiExponent.derivation_trace_of_basis line 126
9. theorem OAI.PiExponent.finite_extension_derivation_ne_simple_pole line 160