OAI/NumberTheory/PiExponent/Jets/FormalJetDerivatives.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PiExponent.FormalJetDerivatives.pderiv_mem_rationalWeightedIdeal line 13
2. theorem OAI.PiExponent.FormalJetDerivatives.mul_pderiv_mem_rationalWeightedIdeal line 22
3. def OAI.PiExponent.FormalJetDerivatives.jetFrame line 29
4. theorem OAI.PiExponent.FormalJetDerivatives.jetFrame_zero line 33
5. theorem OAI.PiExponent.FormalJetDerivatives.jetFrame_pos line 37
6. theorem OAI.PiExponent.FormalJetDerivatives.jetFrame_mem_rationalWeightedIdeal line 41
7. def OAI.PiExponent.FormalJetDerivatives.jetFrameWord line 53
8. theorem OAI.PiExponent.FormalJetDerivatives.jetFrameWord_mem_rationalWeightedIdeal line 57