OAI/NumberTheory/PiExponent/LocalAlgebra/CoordinateContactBound.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PiExponent.CoordinateContactBound.supportBound_X_sub_C line 14
2. theorem OAI.PiExponent.CoordinateContactBound.ordinary_formalJet_X_sub_C line 22
3. theorem OAI.PiExponent.CoordinateContactBound.X_mem_rationalWeightedIdeal line 29
4. theorem OAI.PiExponent.CoordinateContactBound.ordinary_formalJet_coordinate_mem line 40
5. theorem OAI.PiExponent.CoordinateContactBound.coordinate_contact_sum_le line 47