OAI/RepresentationTheory/RestrictedTilting/RestrictedTarget.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.FiberFunctorProof.RestrictedTarget.linearChange line 18
  2. lemma OAI.FiberFunctorProof.RestrictedTarget.linearChange_X line 22
  3. lemma OAI.FiberFunctorProof.RestrictedTarget.linearChange_C line 27
  4. lemma OAI.FiberFunctorProof.RestrictedTarget.linearChange_one line 33
  5. lemma OAI.FiberFunctorProof.RestrictedTarget.linearChange_mul line 38
  6. lemma OAI.FiberFunctorProof.RestrictedTarget.linearChange_homogeneous line 51
  7. def OAI.FiberFunctorProof.RestrictedTarget.homogeneousRepresentation line 62
  8. abbrev OAI.FiberFunctorProof.RestrictedTarget.SL2 line 83
  9. def OAI.FiberFunctorProof.RestrictedTarget.IsRational line 86
  10. def OAI.FiberFunctorProof.RestrictedTarget.dualMatrix line 93
  11. instance OAI.FiberFunctorProof.RestrictedTarget.homogeneous_finite line 99
  12. def OAI.FiberFunctorProof.RestrictedTarget.costandard line 104
  13. inductive OAI.FiberFunctorProof.RestrictedTarget.HasGoodFiltration line 108
  14. def OAI.FiberFunctorProof.RestrictedTarget.IsTilting line 116
  15. def OAI.FiberFunctorProof.RestrictedTarget.steinberg line 120
  16. def OAI.FiberFunctorProof.RestrictedTarget.unipotent line 124
  17. lemma OAI.FiberFunctorProof.RestrictedTarget.unipotent_zero line 127
  18. lemma OAI.FiberFunctorProof.RestrictedTarget.unipotent_add line 132
  19. def OAI.FiberFunctorProof.RestrictedTarget.elementaryEmbedding line 140
  20. def OAI.FiberFunctorProof.RestrictedTarget.restrictElementary line 146
  21. def OAI.FiberFunctorProof.RestrictedTarget.RestrictedTiltingTheorem line 158