OAI/NumberTheory/PiExponent/Jets/FormalBranchOrderRational.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PiExponent.FormalBranchOrder.rational_weight_le_of_contact line 14
2. theorem OAI.PiExponent.FormalBranchOrder.rational_order_subst_of_jet_vanishing line 49
3. theorem OAI.PiExponent.FormalBranchOrder.rational_order_subst_of_mem_weightedIdeal line 77
4. theorem OAI.PiExponent.FormalBranchOrder.hasSubst_of_positive_rational_contact line 85
5. theorem OAI.PiExponent.FormalBranchOrder.rational_powerSeries_order_subst_of_mem_weightedIdeal line 99
6. theorem OAI.PiExponent.FormalBranchOrder.rational_mul_cutoff_le_order_toNat line 108