OAI/NumberTheory/PiExponent/Analysis/LogarithmicContactIdeal.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PiExponent.LogarithmicContactIdeal.truncatedCoordinates line 14
2. def OAI.PiExponent.LogarithmicContactIdeal.logarithmicIdeal line 19
3. theorem OAI.PiExponent.LogarithmicContactIdeal.expansion_polynomial_aeval line 23
4. theorem OAI.PiExponent.LogarithmicContactIdeal.expansion_truncatedCoordinates line 32
5. theorem OAI.PiExponent.LogarithmicContactIdeal.truncatedCoordinates_nonzero line 50
6. theorem OAI.PiExponent.LogarithmicContactIdeal.branchContact_congr line 70
7. theorem OAI.PiExponent.LogarithmicContactIdeal.truncated_contact_eq line 77
8. theorem OAI.PiExponent.LogarithmicContactIdeal.logarithmicIdeal_colength_eq_contact line 102
9. theorem OAI.PiExponent.LogarithmicContactIdeal.logarithmicIdeal_colength_ne_top line 118