OAI/Algebra/AffineCancellation/LaurentDerivation.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ComplexCancellation.LaurentDerivation.linear line 10
2. lemma OAI.ComplexCancellation.LaurentDerivation.linear_single line 13
3. lemma OAI.ComplexCancellation.LaurentDerivation.linear_mul line 19
4. def OAI.ComplexCancellation.LaurentDerivation.extension line 32
5. lemma OAI.ComplexCancellation.LaurentDerivation.extension_monomial line 34
6. lemma OAI.ComplexCancellation.LaurentDerivation.extension_C line 36
7. lemma OAI.ComplexCancellation.LaurentDerivation.extension_T line 38
8. lemma OAI.ComplexCancellation.LaurentDerivation.iterate_monomial line 40
9. lemma OAI.ComplexCancellation.LaurentDerivation.locallyNilpotent line 46