OAI/RepresentationTheory/RestrictedTilting/PolynomialCovers.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.FiberFunctorProof.costandard_zero_tilting line 11
2. lemma OAI.FiberFunctorProof.costandard_one_tilting line 13
3. def OAI.FiberFunctorProof.tensorPowerFrom line 16
4. def OAI.FiberFunctorProof.polynomialPowerMap line 20
5. lemma OAI.FiberFunctorProof.polynomialPowerMap_goodKernel line 27
6. lemma OAI.FiberFunctorProof.tensorPowerFrom_tilting line 35
7. lemma OAI.FiberFunctorProof.tensorPowerFrom_rational line 42
8. lemma OAI.FiberFunctorProof.tensorPowerFrom_weights line 50
9. lemma OAI.FiberFunctorProof.tensorPowerFrom_factor line 65