OAI/RepresentationTheory/RestrictedTilting/CompatibleJets.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.FiberFunctorProof.IsRational.prod line 12
  2. def OAI.FiberFunctorProof.representationPullback line 28
  3. theorem OAI.FiberFunctorProof.good_weyl_lift line 41
  4. def OAI.FiberFunctorProof.planeJetFD line 119
  5. def OAI.FiberFunctorProof.planeJetLayerFD line 124
  6. def OAI.FiberFunctorProof.planeJetTransitionHom line 129
  7. def OAI.FiberFunctorProof.planeJetLayerInclusionHom line 134
  8. def OAI.FiberFunctorProof.planeLayerMultiplyHom line 139
  9. theorem OAI.FiberFunctorProof.planeJetLayer_good line 146
  10. theorem OAI.FiberFunctorProof.planeJet_lift line 161
  11. theorem OAI.FiberFunctorProof.compatible_planeJet_sections line 190