OAI/RepresentationTheory/RestrictedTilting/TorusRelations.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.FiberFunctorProof.eval_laurent_invert line 14
2. lemma OAI.FiberFunctorProof.rationalTorusMatrix_inverse line 21
3. lemma OAI.FiberFunctorProof.rational_torus_unipotent_laurent line 41