OAI/RepresentationTheory/RestrictedTilting/SteinbergRegular.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.FiberFunctorProof.binaryEval line 12
  2. lemma OAI.FiberFunctorProof.binaryEval_basis line 17
  3. def OAI.FiberFunctorProof.binaryHomogenize line 23
  4. lemma OAI.FiberFunctorProof.binaryEval_homogenize line 27
  5. def OAI.FiberFunctorProof.binarySubgroupEval line 40
  6. lemma OAI.FiberFunctorProof.binarySubgroupEval_surjective line 44
  7. def OAI.FiberFunctorProof.binarySubgroupEquiv line 62
  8. lemma OAI.FiberFunctorProof.binaryEval_unipotent line 71
  9. def OAI.FiberFunctorProof.groupAlgebraCoefficients line 86
  10. lemma OAI.FiberFunctorProof.groupAlgebraCoefficients_apply line 90
  11. theorem OAI.FiberFunctorProof.steinberg_restriction_regular line 95
  12. def OAI.FiberFunctorProof.RegularSteinbergStatement line 135
  13. theorem OAI.FiberFunctorProof.regular_steinberg line 141