OAI/RingTheory/Multiplicity/ProductSourceCoverRootSigned.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.Lech.ProductSourceCover.root_signedRank_real line 24
  2. lemma OAI.Lech.ProductSourceCover.rootLayerTerm_euler_polynomial line 35
  3. theorem OAI.Lech.ProductSourceCover.rootLayerTotal_euler_polynomial line 63
  4. lemma OAI.Lech.biprod_homology_property line 101
  5. lemma OAI.Lech.biprod_homology_euler line 108
  6. def OAI.Lech.ProductSourceCover.rootIntervalRow line 138
  7. lemma OAI.Lech.ProductSourceCover.rootIntervalRow_property line 142
  8. lemma OAI.Lech.ProductSourceCover.rootIntervalRow_isZero line 152
  9. lemma OAI.Lech.ProductSourceCover.rootIntervalRow_finite line 160
  10. lemma OAI.Lech.ProductSourceCover.rootTwistRow_euler_natShift line 166
  11. lemma OAI.Lech.ProductSourceCover.rootIntervalRow_euler line 177
  12. def OAI.Lech.ProductSourceCover.rootStripTerm line 203
  13. def OAI.Lech.ProductSourceCover.rootStripDouble line 212
  14. lemma OAI.Lech.ProductSourceCover.rootStripDouble_bounded line 215
  15. lemma OAI.Lech.ProductSourceCover.rootStripTerm_isZero line 220
  16. lemma OAI.Lech.ProductSourceCover.rootStripTerm_finite line 229
  17. theorem OAI.Lech.ProductSourceCover.rootStripTotal_finite line 242
  18. theorem OAI.Lech.ProductSourceCover.rootStripTotal_euler_rows line 256
  19. def OAI.Lech.ProductSourceCover.rootStripPolynomial line 304
  20. lemma OAI.Lech.ProductSourceCover.rootStripTerm_euler_polynomial line 306
  21. theorem OAI.Lech.ProductSourceCover.rootStripTotal_euler_polynomial line 340
  22. instance OAI.Lech.Homogeneous.algebra line 380
  23. lemma OAI.Lech.Homogeneous.val_algebraMap line 391
  24. instance OAI.Lech.Homogeneous.scalarTower line 397
  25. abbrev OAI.Lech.ProjectiveCoefficientChart.grading line 410
  26. abbrev OAI.Lech.ProjectiveCoefficientChart.Chart line 411
  27. abbrev OAI.Lech.ProjectiveCoefficientChart.Ambient line 412
  28. def OAI.Lech.ProjectiveCoefficientChart.coordinate line 413
  29. def OAI.Lech.ProjectiveCoefficientChart.forward line 415
  30. def OAI.Lech.ProjectiveCoefficientChart.evaluate line 417
  31. def OAI.Lech.ProjectiveCoefficientChart.dehomogenize line 419
  32. def OAI.Lech.ProjectiveCoefficientChart.inclusion line 422
  33. def OAI.Lech.ProjectiveCoefficientChart.backward line 425
  34. lemma OAI.Lech.ProjectiveCoefficientChart.coordinate_val line 427
  35. lemma OAI.Lech.ProjectiveCoefficientChart.backward_mk line 431
  36. lemma OAI.Lech.ProjectiveCoefficientChart.backward_coordinate line 440
  37. lemma OAI.Lech.ProjectiveCoefficientChart.backward_forward line 444