OAI/Algebra/AffineCancellation/Bundle.lean

GitHub source file

47 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ComplexCancellation.Bundle.quadricEval line 12
  2. lemma OAI.ComplexCancellation.Bundle.quadricEval_relation line 13
  3. def OAI.ComplexCancellation.Bundle.inclusion line 17
  4. lemma OAI.ComplexCancellation.Bundle.inclusion_π line 21
  5. lemma OAI.ComplexCancellation.Bundle.inclusion_x line 23
  6. lemma OAI.ComplexCancellation.Bundle.inclusion_y line 24
  7. lemma OAI.ComplexCancellation.Bundle.inclusion_z line 25
  8. lemma OAI.ComplexCancellation.Bundle.inclusion_u line 26
  9. abbrev OAI.ComplexCancellation.Bundle.K line 28
  10. def OAI.ComplexCancellation.Bundle.ι line 29
  11. lemma OAI.ComplexCancellation.Bundle.ι_injective line 30
  12. lemma OAI.ComplexCancellation.Bundle.x_ne_zero line 31
  13. def OAI.ComplexCancellation.Bundle.chartEval line 32
  14. lemma OAI.ComplexCancellation.Bundle.chartEval_relation line 34
  15. def OAI.ComplexCancellation.Bundle.chart line 39
  16. lemma OAI.ComplexCancellation.Bundle.chart_π line 43
  17. lemma OAI.ComplexCancellation.Bundle.chart_inclusion line 44
  18. lemma OAI.ComplexCancellation.Bundle.inclusion_injective line 65
  19. def OAI.ComplexCancellation.Bundle.h line 70
  20. def OAI.ComplexCancellation.Bundle.C₁ line 71
  21. def OAI.ComplexCancellation.Bundle.α line 72
  22. def OAI.ComplexCancellation.Bundle.β line 73
  23. lemma OAI.ComplexCancellation.Bundle.inclusion_s line 74
  24. lemma OAI.ComplexCancellation.Bundle.inclusion_f line 76
  25. lemma OAI.ComplexCancellation.Bundle.inclusion_g line 79
  26. lemma OAI.ComplexCancellation.Bundle.certificate line 82
  27. lemma OAI.ComplexCancellation.Bundle.v_ne_zero line 85
  28. abbrev OAI.ComplexCancellation.Bundle.B line 92
  29. instance OAI.ComplexCancellation.Bundle.(instance at line 93) line 93
  30. def OAI.ComplexCancellation.Bundle.j line 95
  31. def OAI.ComplexCancellation.Bundle.τ line 96
  32. def OAI.ComplexCancellation.Bundle.V line 97
  33. lemma OAI.ComplexCancellation.Bundle.τ_ne_zero line 98
  34. lemma OAI.ComplexCancellation.Bundle.equation line 104
  35. def OAI.ComplexCancellation.Bundle.values line 106
  36. def OAI.ComplexCancellation.Bundle.eval line 107
  37. lemma OAI.ComplexCancellation.Bundle.eval_xp line 108
  38. lemma OAI.ComplexCancellation.Bundle.eval_yp line 114
  39. lemma OAI.ComplexCancellation.Bundle.eval_zp line 119
  40. lemma OAI.ComplexCancellation.Bundle.eval_relation line 125
  41. def OAI.ComplexCancellation.Bundle.pullback line 133
  42. lemma OAI.ComplexCancellation.Bundle.pullback_π line 137
  43. lemma OAI.ComplexCancellation.Bundle.pullback_coefficientMap line 139
  44. def OAI.ComplexCancellation.Bundle.base line 153
  45. lemma OAI.ComplexCancellation.Bundle.base_injective line 154
  46. lemma OAI.ComplexCancellation.Bundle.pullback_baseMap line 162
  47. lemma OAI.ComplexCancellation.Bundle.pullback_injective line 177