OAI/RingTheory/Multiplicity/AlternatingCechPost.lean

GitHub source file

54 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Lech.AlternatingCech.post line 22
  2. lemma OAI.Lech.AlternatingCech.evaluation_post line 27
  3. lemma OAI.Lech.AlternatingCech.delta_post line 29
  4. lemma OAI.Lech.AlternatingCech.projection_exact line 46
  5. lemma OAI.Lech.AlternatingCech.projection_complex_exactAt line 70
  6. lemma OAI.Lech.AlternatingCech.complex_exactAt_zero_of_nonempty line 81
  7. lemma OAI.Lech.AlternatingCech.projection_complex_acyclic line 93
  8. lemma OAI.Lech.AlternatingCech.post_prism_mem line 107
  9. lemma OAI.Lech.AlternatingCech.post_pullback_zero line 133
  10. lemma OAI.Lech.AlternatingCech.projection_prism_exact line 155
  11. lemma OAI.Lech.AlternatingCech.projection_prism_exactAt line 173
  12. lemma OAI.Lech.AlternatingCech.projection_prism_acyclic line 185
  13. abbrev OAI.Lech.UniversalCoefficientChart.Ring line 198
  14. def OAI.Lech.UniversalCoefficientChart.coefficient line 200
  15. def OAI.Lech.UniversalCoefficientChart.form line 202
  16. lemma OAI.Lech.UniversalCoefficientChart.coefficient_self line 204
  17. lemma OAI.Lech.UniversalCoefficientChart.coefficient_other line 205
  18. lemma OAI.Lech.UniversalCoefficientChart.form_coeff line 207
  19. lemma OAI.Lech.UniversalCoefficientChart.form_degree line 209
  20. lemma OAI.Lech.UniversalCoefficientChart.form_primitive line 211
  21. def OAI.Lech.UniversalCoefficientChart.eval line 217
  22. lemma OAI.Lech.UniversalCoefficientChart.eval_coefficient line 218
  23. lemma OAI.Lech.UniversalCoefficientChart.eval_form line 227
  24. lemma OAI.Lech.UniversalCoefficientChart.ext line 238
  25. abbrev OAI.Lech.ProductLinearChart.Ring line 250
  26. def OAI.Lech.ProductLinearChart.a line 252
  27. def OAI.Lech.ProductLinearChart.b line 253
  28. lemma OAI.Lech.ProductLinearChart.selected line 255
  29. lemma OAI.Lech.ProductLinearChart.other line 257
  30. def OAI.Lech.ProductLinearChart.product line 260
  31. lemma OAI.Lech.ProductLinearChart.linear_degree line 262
  32. lemma OAI.Lech.ProductLinearChart.product_degree line 267
  33. lemma OAI.Lech.ProductLinearChart.product_homogenize line 278
  34. abbrev OAI.Lech.ProductLinearChart.chart line 291
  35. def OAI.Lech.ProductLinearChart.denominator line 293
  36. lemma OAI.Lech.ProductLinearChart.denominator_val line 295
  37. def OAI.Lech.ProductLinearChart.normalized line 299
  38. lemma OAI.Lech.ProductLinearChart.normalized_degree line 302
  39. lemma OAI.Lech.ProductLinearChart.normalized_self line 304
  40. def OAI.Lech.ProductLinearChart.target line 307
  41. lemma OAI.Lech.ProductLinearChart.target_form line 310
  42. lemma OAI.Lech.ProductLinearChart.target_factorization line 314
  43. instance OAI.Lech.ProductLinearChart.targetAlgebra line 322
  44. instance OAI.Lech.ProductLinearChart.targetTower line 324
  45. lemma OAI.Lech.ProductLinearChart.finSucc_rename line 337
  46. lemma OAI.Lech.ProductLinearChart.rename_a line 349
  47. lemma OAI.Lech.ProductLinearChart.rename_b line 352
  48. lemma OAI.Lech.ProductLinearChart.rename_factor line 355
  49. lemma OAI.Lech.ProductLinearChart.product_succ line 363
  50. lemma OAI.Lech.ProductLinearChart.finSucc_a line 372
  51. lemma OAI.Lech.ProductLinearChart.finSucc_b line 375
  52. lemma OAI.Lech.ProductLinearChart.product_succ_coeff_zero line 378
  53. lemma OAI.Lech.ProductLinearChart.product_succ_coeff_succ line 386
  54. theorem OAI.Lech.ProductLinearChart.coefficient_regular line 398