OAI/NumberTheory/PiExponent/Jets/AffineJetQuotient.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PiExponent.AffineJetQuotient.restrictionSectionsIso_natural line 12
2. def OAI.PiExponent.AffineJetQuotient.untwistSectionsIso line 21
3. theorem OAI.PiExponent.AffineJetQuotient.untwistSectionsIso_natural line 28
4. theorem OAI.PiExponent.AffineJetQuotient.localQuotientEquiv_apply line 48
5. def OAI.PiExponent.AffineJetQuotient.globalSectionCoefficient line 54
6. theorem OAI.PiExponent.AffineJetQuotient.globalQuotientValue_jetRestriction line 60
7. theorem OAI.PiExponent.AffineJetQuotient.coefficient_quotient_surjective_of_jetRestriction line 84