OAI/NumberTheory/PiExponent/LocalAlgebra/FibreContact.lean
7 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.PiExponent.FibreContact.contact_zero_consline 11 - theorem
OAI.PiExponent.FibreContact.coordinates_oneline 35 - theorem
OAI.PiExponent.FibreContact.logarithmic_contact_eq_ordinaryline 47 - theorem
OAI.PiExponent.FibreContact.weightedPole_leline 64 - theorem
OAI.PiExponent.FibreContact.weightedPole_zero_consline 73 - theorem
OAI.PiExponent.FibreContact.coordinatePole_oneline 101 - theorem
OAI.PiExponent.FibreContact.weightedDegree_oneline 116