OAI/Algebra/AffineCancellation/Degeneration.lean

GitHub source file

54 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.ComplexCancellation.Degeneration.P line 9
  2. def OAI.ComplexCancellation.Degeneration.xp line 10
  3. def OAI.ComplexCancellation.Degeneration.yp line 11
  4. def OAI.ComplexCancellation.Degeneration.zp line 12
  5. def OAI.ComplexCancellation.Degeneration.relation line 13
  6. lemma OAI.ComplexCancellation.Degeneration.identity line 14
  7. abbrev OAI.ComplexCancellation.Degeneration.G line 17
  8. def OAI.ComplexCancellation.Degeneration.π line 18
  9. def OAI.ComplexCancellation.Degeneration.p line 19
  10. def OAI.ComplexCancellation.Degeneration.s line 20
  11. def OAI.ComplexCancellation.Degeneration.u line 21
  12. def OAI.ComplexCancellation.Degeneration.F line 22
  13. def OAI.ComplexCancellation.Degeneration.J line 23
  14. def OAI.ComplexCancellation.Degeneration.x line 24
  15. def OAI.ComplexCancellation.Degeneration.y line 25
  16. def OAI.ComplexCancellation.Degeneration.z line 26
  17. lemma OAI.ComplexCancellation.Degeneration.relation_zero line 27
  18. lemma OAI.ComplexCancellation.Degeneration.equation line 28
  19. def OAI.ComplexCancellation.Degeneration.coeffEval line 33
  20. lemma OAI.ComplexCancellation.Degeneration.coeffEval_relation line 34
  21. def OAI.ComplexCancellation.Degeneration.coefficientMap line 36
  22. lemma OAI.ComplexCancellation.Degeneration.coefficientMap_π line 40
  23. lemma OAI.ComplexCancellation.Degeneration.coefficientMap_x line 42
  24. lemma OAI.ComplexCancellation.Degeneration.coefficientMap_y line 43
  25. lemma OAI.ComplexCancellation.Degeneration.coefficientMap_z line 44
  26. lemma OAI.ComplexCancellation.Degeneration.coefficientMap_u line 45
  27. lemma OAI.ComplexCancellation.Degeneration.coefficientMap_s line 46
  28. lemma OAI.ComplexCancellation.Degeneration.coefficientMap_f line 50
  29. lemma OAI.ComplexCancellation.Degeneration.coefficientMap_g line 54
  30. abbrev OAI.ComplexCancellation.Degeneration.K₀ line 59
  31. abbrev OAI.ComplexCancellation.Degeneration.K line 60
  32. def OAI.ComplexCancellation.Degeneration.ι line 61
  33. lemma OAI.ComplexCancellation.Degeneration.ι_injective line 62
  34. lemma OAI.ComplexCancellation.Degeneration.τ_ne_zero line 64
  35. def OAI.ComplexCancellation.Degeneration.values line 65
  36. def OAI.ComplexCancellation.Degeneration.eval line 67
  37. lemma OAI.ComplexCancellation.Degeneration.eval_xp line 68
  38. lemma OAI.ComplexCancellation.Degeneration.eval_yp line 74
  39. lemma OAI.ComplexCancellation.Degeneration.eval_zp line 79
  40. lemma OAI.ComplexCancellation.Degeneration.eval_relation line 85
  41. def OAI.ComplexCancellation.Degeneration.embedding line 94
  42. lemma OAI.ComplexCancellation.Degeneration.embedding_π line 98
  43. lemma OAI.ComplexCancellation.Degeneration.embedding_coefficientMap line 99
  44. lemma OAI.ComplexCancellation.Degeneration.coefficientMap_injective line 113
  45. lemma OAI.ComplexCancellation.Degeneration.p_regular line 117
  46. def OAI.ComplexCancellation.Degeneration.baseMap line 123
  47. lemma OAI.ComplexCancellation.Degeneration.baseMap_X line 125
  48. lemma OAI.ComplexCancellation.Degeneration.baseMap_C line 126
  49. def OAI.ComplexCancellation.Degeneration.baseEmbedding line 127
  50. lemma OAI.ComplexCancellation.Degeneration.baseEmbedding_injective line 130
  51. lemma OAI.ComplexCancellation.Degeneration.embedding_baseMap line 133
  52. lemma OAI.ComplexCancellation.Degeneration.clears line 146
  53. lemma OAI.ComplexCancellation.Degeneration.embedding_injective line 155
  54. instance OAI.ComplexCancellation.Degeneration.(instance at line 160) line 160