OAI/RepresentationTheory/RestrictedTilting/PolynomialJets.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.FiberFunctorProof.polynomialExtend line 13
2. lemma OAI.FiberFunctorProof.polynomialExtend_tmul line 18
3. def OAI.FiberFunctorProof.polynomialAugment line 22
4. lemma OAI.FiberFunctorProof.polynomialAugment_tmul line 29
5. lemma OAI.FiberFunctorProof.polynomialAugment_smul line 32
6. lemma OAI.FiberFunctorProof.polynomialAugment_pairRelation line 39
7. lemma OAI.FiberFunctorProof.polynomial_origin_representative line 46
8. theorem OAI.FiberFunctorProof.polynomialExtend_jet_bijective line 69