OAI/RingTheory/Multiplicity/LechTorsionOf.lean

GitHub source file

62 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.Lech.torsion_of_quotient_scalar line 16
  2. lemma OAI.Lech.SourceGraded.polynomialMap_smul line 32
  3. def OAI.Lech.SourceGraded.degreeMap line 38
  4. lemma OAI.Lech.SourceGraded.degreeMap_surjective line 44
  5. lemma OAI.Lech.SourceGraded.polynomial_piece_value line 53
  6. lemma OAI.Lech.SourceGraded.associated_piece_value line 67
  7. lemma OAI.Lech.SourceGraded.degree_kernel_zero line 100
  8. structure OAI.Lech.AllModuleLength line 123
  9. def OAI.Lech.AllModuleLength.torsionLength line 144
  10. lemma OAI.Lech.AllModuleLength.quotient_mono line 149
  11. lemma OAI.Lech.AllModuleLength.value_eq_of_linearEquiv line 168
  12. lemma OAI.Lech.AllModuleLength.zero_of_surjective line 177
  13. lemma OAI.Lech.AllModuleLength.zero_of_injective line 183
  14. lemma OAI.Lech.AllModuleLength.zero_of_ranges line 189
  15. lemma OAI.Lech.AllModuleLength.zero_of_decomposition line 199
  16. lemma OAI.Lech.AllModuleLength.tensor_zero_right line 210
  17. lemma OAI.Lech.AllModuleLength.tensor_zero_left line 220
  18. lemma OAI.Lech.AllModuleLength.localized_zero line 228
  19. lemma OAI.Lech.Homogeneous.away_kernel_length_zero line 256
  20. abbrev OAI.Lech.SourceGraded.sourceGrade line 283
  21. abbrev OAI.Lech.SourceGraded.targetGrade line 285
  22. instance OAI.Lech.SourceGraded.source_graded line 287
  23. instance OAI.Lech.SourceGraded.target_graded line 289
  24. abbrev OAI.Lech.SourceGraded.mapR line 292
  25. lemma OAI.Lech.SourceGraded.mapR_smul line 296
  26. lemma OAI.Lech.SourceGraded.mapR_surjective line 304
  27. abbrev OAI.Lech.SourceGraded.gradedMapR line 307
  28. def OAI.Lech.SourceGraded.chartMapR line 313
  29. lemma OAI.Lech.SourceGraded.mapR_degree_kernel_zero line 326
  30. lemma OAI.Lech.SourceGraded.chart_kernel_zero line 354
  31. lemma OAI.Lech.SourceGraded.chart_surjective line 369
  32. def OAI.Lech.PartialLaurent.exponents line 384
  33. abbrev OAI.Lech.PartialLaurent.Poly line 390
  34. abbrev OAI.Lech.PartialLaurent.Laurent line 391
  35. def OAI.Lech.PartialLaurent.fromNat line 392
  36. lemma OAI.Lech.PartialLaurent.fromNat_injective line 396
  37. def OAI.Lech.PartialLaurent.toLaurent line 400
  38. instance OAI.Lech.PartialLaurent.(instance at line 402) line 402
  39. lemma OAI.Lech.PartialLaurent.algebraMap_single line 403
  40. lemma OAI.Lech.PartialLaurent.toLaurent_injective line 406
  41. def OAI.Lech.PartialLaurent.indicator line 408
  42. def OAI.Lech.PartialLaurent.denominator line 409
  43. def OAI.Lech.PartialLaurent.negativeIndicator line 410
  44. lemma OAI.Lech.PartialLaurent.indicator_add_negative line 412
  45. lemma OAI.Lech.PartialLaurent.denominator_unit line 415
  46. lemma OAI.Lech.PartialLaurent.clear_exponent line 423
  47. lemma OAI.Lech.PartialLaurent.clear_single line 439
  48. lemma OAI.Lech.PartialLaurent.clear_denominators line 446
  49. instance OAI.Lech.PartialLaurent.localization line 469
  50. def OAI.Lech.PartialLaurent.polynomialEquiv line 482
  51. lemma OAI.Lech.PartialLaurent.polynomialEquiv_X line 485
  52. lemma OAI.Lech.PartialLaurent.polynomialEquiv_denominator line 492
  53. def OAI.Lech.PartialLaurent.exponentInclusion line 503
  54. def OAI.Lech.PartialLaurent.restrict line 508
  55. lemma OAI.Lech.PartialLaurent.restrict_single line 510
  56. lemma OAI.Lech.PartialLaurent.restrict_injective line 513
  57. lemma OAI.Lech.PartialLaurent.restrict_comp line 517
  58. lemma OAI.Lech.PartialLaurent.restrict_algebraMap line 525
  59. def OAI.Lech.PartialLaurent.degree line 537
  60. def OAI.Lech.PartialLaurent.homogeneous line 539
  61. def OAI.Lech.PartialLaurent.homogeneousCoefficients line 543
  62. def OAI.Lech.PartialLaurent.homogeneousEquiv line 556