OAI/RepresentationTheory/RestrictedTilting/FiniteJetMaps.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.FiberFunctorProof.polynomialJetExtend line 14
2. lemma OAI.FiberFunctorProof.polynomialJetExtend_mk line 34
3. lemma OAI.FiberFunctorProof.polynomialJetExtend_mk_tmul line 40
4. lemma OAI.FiberFunctorProof.polynomialJetExtend_transition line 46
5. def OAI.FiberFunctorProof.coefficientAdicEquiv line 63
6. lemma OAI.FiberFunctorProof.coefficientAdicEquiv_mk line 69
7. theorem OAI.FiberFunctorProof.polynomialJetExtend_bijective line 74