OAI/RepresentationTheory/RestrictedTilting/RationalMatrices.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.FiberFunctorProof.rationalCoefficient line 12
2. lemma OAI.FiberFunctorProof.eval_rationalCoefficient line 15
3. def OAI.FiberFunctorProof.unipotentPolynomialCoordinates line 20
4. def OAI.FiberFunctorProof.torusLaurentCoordinates line 23
5. def OAI.FiberFunctorProof.rationalUnipotentMatrix line 27
6. def OAI.FiberFunctorProof.rationalTorusMatrix line 31
7. lemma OAI.FiberFunctorProof.eval_unipotentPolynomialCoordinates line 35
8. lemma OAI.FiberFunctorProof.eval_torusLaurentCoordinates line 40
9. lemma OAI.FiberFunctorProof.eval_rationalUnipotentMatrix line 48
10. lemma OAI.FiberFunctorProof.eval_rationalTorusMatrix line 63