OAI/RepresentationTheory/RestrictedTilting/TorusWeightProjection.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.FiberFunctorProof.torusExpansion line 11
2. lemma OAI.FiberFunctorProof.torusExpansion_spec line 16
3. lemma OAI.FiberFunctorProof.torusExpansion_unique line 22
4. def OAI.FiberFunctorProof.torusWeightProjection line 32
5. lemma OAI.FiberFunctorProof.torusWeightProjection_eigen line 54
6. lemma OAI.FiberFunctorProof.torusWeightProjection_zero_fixed line 64