OAI/RepresentationTheory/RestrictedTilting/AdicJets.lean
7 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.FiberFunctorProof.jetRelation_succline 10 - theorem
OAI.FiberFunctorProof.jetRelation_eq_pow_smulline 33 - lemma
OAI.FiberFunctorProof.planeIdeal_eqline 50 - lemma
OAI.FiberFunctorProof.planeJetRelation_eq_pow_smulline 63 - def
OAI.FiberFunctorProof.planeJetAdicEquivline 68 - lemma
OAI.FiberFunctorProof.planeJetAdicEquiv_mkline 74 - lemma
OAI.FiberFunctorProof.planeJetAdicEquiv_transitionline 79