OAI/RepresentationTheory/RestrictedTilting/RestrictedLift.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.FiberFunctorProof.liftEntry line 21
  2. def OAI.FiberFunctorProof.liftMatrix line 27
  3. lemma OAI.FiberFunctorProof.liftEntry_degree line 30
  4. lemma OAI.FiberFunctorProof.liftMatrix_at_subgroup line 38
  5. lemma OAI.FiberFunctorProof.polynomial_degree_translate line 46
  6. lemma OAI.FiberFunctorProof.polynomial_degree_mul_constant_le line 50
  7. lemma OAI.FiberFunctorProof.polynomial_degree_constant_mul_le line 56
  8. lemma OAI.FiberFunctorProof.polynomial_degree_sum_lt line 60
  9. lemma OAI.FiberFunctorProof.liftMatrix_add_subgroup line 67
  10. lemma OAI.FiberFunctorProof.liftMatrix_add line 92
  11. lemma OAI.FiberFunctorProof.liftMatrix_zero line 116
  12. def OAI.FiberFunctorProof.extendedRepresentation line 121
  13. theorem OAI.FiberFunctorProof.finite_additive_representation_lift line 129