OAI/RepresentationTheory/RestrictedTilting/JetRelations.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

Binary sums, jet relations and their layer quotients.

  1. def OAI.FiberFunctorProof.binarySum line 17
  2. lemma OAI.FiberFunctorProof.binarySum_apply line 20
  3. lemma OAI.FiberFunctorProof.binarySum_zero line 24
  4. lemma OAI.FiberFunctorProof.binarySum_succ line 27
  5. lemma OAI.FiberFunctorProof.binarySum_single_zero line 36
  6. def OAI.FiberFunctorProof.pairRelation line 46
  7. lemma OAI.FiberFunctorProof.x_smul_mem_pairRelation line 49
  8. lemma OAI.FiberFunctorProof.y_smul_mem_pairRelation line 53
  9. lemma OAI.FiberFunctorProof.regular_pair_y_pow line 57
  10. theorem OAI.FiberFunctorProof.binarySum_kernel_coefficients line 68
  11. lemma OAI.FiberFunctorProof.binarySum_succ_last line 110
  12. lemma OAI.FiberFunctorProof.binarySum_prepend_zero line 120
  13. lemma OAI.FiberFunctorProof.binarySum_append_zero line 125
  14. def OAI.FiberFunctorProof.jetRelation line 131
  15. lemma OAI.FiberFunctorProof.jetRelation_zero line 133
  16. lemma OAI.FiberFunctorProof.mem_pairRelation line 138
  17. lemma OAI.FiberFunctorProof.jetRelation_one line 148
  18. lemma OAI.FiberFunctorProof.jetRelation_succ_le line 162
  19. lemma OAI.FiberFunctorProof.binarySum_pairRelation line 169
  20. theorem OAI.FiberFunctorProof.binarySum_mem_next_iff line 182
  21. abbrev OAI.FiberFunctorProof.jetLayer line 210
  22. def OAI.FiberFunctorProof.jetLayerMap line 214
  23. lemma OAI.FiberFunctorProof.jetLayerMap_surjective line 218
  24. lemma OAI.FiberFunctorProof.jetLayerMap_eq_zero_iff line 223
  25. def OAI.FiberFunctorProof.originCoefficientMap line 227
  26. lemma OAI.FiberFunctorProof.originCoefficientMap_surjective line 231
  27. lemma OAI.FiberFunctorProof.originCoefficientMap_eq_zero_iff line 237
  28. lemma OAI.FiberFunctorProof.jetLayerMap_ker line 246
  29. def OAI.FiberFunctorProof.jetLayerEquiv line 257
  30. lemma OAI.FiberFunctorProof.jetLayerEquiv_apply line 266