OAI/RingTheory/Multiplicity/TwistedLocalizationPieceMap.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.Lech.TwistedLocalization.pieceMap_injective line 25
  2. def OAI.Lech.TwistedLocalization.pieceEquiv line 41
  3. def OAI.Lech.TwistedLocalization.pieceCongr line 50
  4. lemma OAI.Lech.TwistedLocalization.piece_restrictScalars line 58
  5. lemma OAI.Lech.TwistedLocalization.pieceCongr_pieceTo line 76
  6. def OAI.Lech.GradedChart.denominator line 97
  7. lemma OAI.Lech.GradedChart.denominator_mem line 100
  8. lemma OAI.Lech.GradedChart.denominator_mul_sdiff line 104
  9. lemma OAI.Lech.GradedChart.denominator_dvd line 111
  10. abbrev OAI.Lech.GradedChart.term line 114
  11. def OAI.Lech.GradedChart.restrict line 118
  12. lemma OAI.Lech.GradedChart.restrict_val line 124
  13. lemma OAI.Lech.GradedChart.restrict_comp line 128
  14. lemma OAI.Lech.GradedChart.restrict_self line 140
  15. instance OAI.Lech.PartialLaurent.laurentScalarTower line 155
  16. def OAI.Lech.PartialLaurent.localizationEquiv line 161
  17. lemma OAI.Lech.PartialLaurent.localizationEquiv_fraction line 165
  18. lemma OAI.Lech.PartialLaurent.localizationEquiv_mem line 177
  19. def OAI.Lech.PartialLaurent.twistToLaurent line 190
  20. lemma OAI.Lech.PartialLaurent.twistToLaurent_surjective line 196
  21. def OAI.Lech.PartialLaurent.twistLaurentEquiv line 212
  22. lemma OAI.Lech.PartialLaurent.polynomialEquiv_grade_iff line 227
  23. def OAI.Lech.PartialLaurent.polynomialGraded line 254
  24. def OAI.Lech.PartialLaurent.polynomialDenominator line 268
  25. lemma OAI.Lech.PartialLaurent.polynomialDenominator_homogeneous line 270
  26. instance OAI.Lech.PartialLaurent.polynomialLaurentAlgebra line 275
  27. lemma OAI.Lech.PartialLaurent.polynomial_algebraMap line 278
  28. instance OAI.Lech.PartialLaurent.polynomialLaurentTower line 282
  29. instance OAI.Lech.PartialLaurent.polynomialLocalization line 293
  30. def OAI.Lech.PartialLaurent.polynomialLocalizationEquiv line 302
  31. lemma OAI.Lech.PartialLaurent.polynomialLocalizationEquiv_fraction line 306
  32. lemma OAI.Lech.PartialLaurent.polynomialLocalizationEquiv_mem line 322
  33. def OAI.Lech.PartialLaurent.polynomialTwistToLaurent line 334
  34. lemma OAI.Lech.PartialLaurent.polynomialTwistToLaurent_surjective line 342
  35. def OAI.Lech.PartialLaurent.polynomialTwistEquiv line 364
  36. def OAI.Lech.PartialLaurent.restrictAlgHom line 380
  37. lemma OAI.Lech.PartialLaurent.polynomialLocalizationEquiv_algebraMap line 387
  38. lemma OAI.Lech.PartialLaurent.polynomialLocalizationEquiv_naturality line 395
  39. lemma OAI.Lech.PartialLaurent.polynomialTwistEquiv_naturality line 414
  40. def OAI.Lech.PartialLaurent.polynomialCechEquiv line 426
  41. lemma OAI.Lech.PartialLaurent.polynomialCechEquiv_naturality line 433