OAI/RingTheory/Multiplicity/NativeDescentCanonicalAlg.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Lech.NativeDescent.canonicalAlg line 24
  2. lemma OAI.Lech.NativeDescent.canonicalAlg_linear line 29
  3. def OAI.Lech.NativeDescent.canonicalAlgebra line 33
  4. lemma OAI.Lech.NativeDescent.canonicalAlgebra_module line 36
  5. def OAI.Lech.NativeDescent.canonicalAlgUnit line 44
  6. lemma OAI.Lech.NativeDescent.canonicalAlgUnit_bijective line 54
  7. def OAI.Lech.NativeDescent.canonicalAlgEquiv line 70
  8. abbrev OAI.Lech.FactorDescent.R line 87
  9. abbrev OAI.Lech.FactorDescent.U line 88
  10. abbrev OAI.Lech.FactorDescent.includeT line 89
  11. abbrev OAI.Lech.FactorDescent.right line 90
  12. abbrev OAI.Lech.FactorDescent.canonical line 91
  13. lemma OAI.Lech.FactorDescent.canonical_include line 93
  14. def OAI.Lech.FactorDescent.coefficients line 98
  15. lemma OAI.Lech.FactorDescent.coefficients_right line 102
  16. lemma OAI.Lech.FactorDescent.natural line 107
  17. def OAI.Lech.FactorDescent.invariantMap line 134
  18. def OAI.Lech.FactorDescent.descended line 153
  19. lemma OAI.Lech.FactorDescent.descended_include line 161
  20. lemma OAI.Lech.UniversalFactorMap.polynomial_square line 188
  21. lemma OAI.Lech.UniversalFactorMap.form line 196
  22. lemma OAI.Lech.UniversalFactorMap.value line 204
  23. def OAI.Lech.UniversalFactorMap.denominator line 210
  24. lemma OAI.Lech.UniversalFactorMap.denominator_val line 216
  25. lemma OAI.Lech.UniversalFactorMap.factorization line 221
  26. def OAI.Lech.UniversalFactorMap.splittingMap line 229
  27. lemma OAI.Lech.UniversalFactorMap.splittingMap_root line 232
  28. def OAI.Lech.UniversalFactorMap.map line 238
  29. lemma OAI.Lech.UniversalFactorMap.map_include line 243
  30. lemma OAI.Lech.FactorDescent.includeT_injective line 261
  31. def OAI.Lech.FactorDescent.extend line 269
  32. lemma OAI.Lech.FactorDescent.extend_subtype line 274
  33. lemma OAI.Lech.FactorDescent.extend_injective line 286
  34. lemma OAI.Lech.FactorDescent.point_ext line 295
  35. lemma OAI.Lech.FactorDescent.extend_descended line 305
  36. theorem OAI.Lech.FactorDescent.unique line 321
  37. lemma OAI.Lech.UniversalFactorMap.denominator_product line 350
  38. lemma OAI.Lech.UniversalFactorMap.recover_selected line 355
  39. lemma OAI.Lech.UniversalFactorMap.map_chartFunction line 383
  40. lemma OAI.Lech.StandardFactorCharts.map_coordinate_relation line 411
  41. lemma OAI.Lech.StandardFactorCharts.normalized_root line 428