OAI/RepresentationTheory/RestrictedTilting/PlaneFibre.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.FiberFunctorProof.planeFibreRelations line 14
  2. lemma OAI.FiberFunctorProof.planeFibre_mk_smul line 17
  3. lemma OAI.FiberFunctorProof.planeFibre_map_mem line 28
  4. def OAI.FiberFunctorProof.planeFibreMap line 38
  5. lemma OAI.FiberFunctorProof.planeFibreMap_mk line 43
  6. def OAI.FiberFunctorProof.planeFibreEquivOfSplit line 49
  7. def OAI.FiberFunctorProof.planeVectorEval line 63
  8. def OAI.FiberFunctorProof.planeVectorConstant line 68
  9. lemma OAI.FiberFunctorProof.planeVectorEval_relations line 74
  10. def OAI.FiberFunctorProof.planeFreeFibreEval line 88
  11. lemma OAI.FiberFunctorProof.planeFreeFibre_constant_eval line 92
  12. def OAI.FiberFunctorProof.planeFreeFibreEquiv line 108
  13. lemma OAI.FiberFunctorProof.planeFreeFibreEquiv_mk line 116