OAI/RingTheory/Multiplicity/StandardFactorChartsL.lean

GitHub source file

47 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Lech.StandardFactorCharts.L line 25
  2. abbrev OAI.Lech.StandardFactorCharts.E line 26
  3. def OAI.Lech.StandardFactorCharts.embedding line 28
  4. lemma OAI.Lech.StandardFactorCharts.embedding_injective line 31
  5. lemma OAI.Lech.StandardFactorCharts.embedding_map line 34
  6. def OAI.Lech.StandardFactorCharts.chartUnit line 41
  7. lemma OAI.Lech.StandardFactorCharts.chartUnit_val line 44
  8. def OAI.Lech.StandardFactorCharts.coordinate line 48
  9. lemma OAI.Lech.StandardFactorCharts.coordinate_selected line 51
  10. lemma OAI.Lech.StandardFactorCharts.cross_identity line 56
  11. lemma OAI.Lech.StandardFactorCharts.coordinate_relation line 71
  12. lemma OAI.Lech.StandardFactorCharts.normalize_product line 90
  13. lemma OAI.Lech.StandardFactorCharts.chart_factorization line 108
  14. def OAI.Lech.RootInvariants.pair line 144
  15. lemma OAI.Lech.RootInvariants.pair_product line 147
  16. abbrev OAI.Lech.RootInvariants.chartRing line 155
  17. def OAI.Lech.RootInvariants.chartCoordinate line 158
  18. def OAI.Lech.RootInvariants.chartUnit line 161
  19. lemma OAI.Lech.RootInvariants.chartCoordinate_selected line 164
  20. lemma OAI.Lech.RootInvariants.sections_binary_form_unit line 168
  21. lemma OAI.Lech.RootInvariants.chart_factorization line 179
  22. lemma OAI.Lech.FactorNormalization.evaluation_product line 204
  23. lemma OAI.Lech.FactorNormalization.factor_value_unit line 210
  24. def OAI.Lech.FactorNormalization.denominator line 218
  25. lemma OAI.Lech.FactorNormalization.denominator_val line 221
  26. def OAI.Lech.FactorNormalization.roots line 225
  27. lemma OAI.Lech.FactorNormalization.unit_product line 227
  28. lemma OAI.Lech.FactorNormalization.transform_factor line 232
  29. lemma OAI.Lech.FactorNormalization.normalized_factorization line 244
  30. lemma OAI.Lech.FactorNormalization.recover_X line 260
  31. lemma OAI.Lech.FactorNormalization.recover_Y line 267
  32. theorem OAI.Lech.FactorNormalization.universal line 277
  33. lemma OAI.Lech.FactorNormalization.mapped_value line 289
  34. lemma OAI.Lech.FactorNormalization.mapped_form line 295
  35. theorem OAI.Lech.FactorNormalization.universal_over line 302
  36. lemma OAI.Lech.FactorNormalization.change_denominator line 318
  37. lemma OAI.Lech.FactorNormalization.change_root line 330
  38. lemma OAI.Lech.FactorNormalization.roots_reparam line 343
  39. lemma OAI.Lech.FFTensorMaps.bijective_baseChange_iff line 359
  40. lemma OAI.Lech.FFTensorMaps.bijective line 365
  41. def OAI.Lech.NativeDescent.canonical line 387
  42. lemma OAI.Lech.NativeDescent.canonical_counit line 390
  43. lemma OAI.Lech.NativeDescent.canonical_coassoc line 395
  44. def OAI.Lech.NativeDescent.canonicalUnit line 402
  45. lemma OAI.Lech.NativeDescent.canonical_compat line 407
  46. lemma OAI.Lech.NativeDescent.canonicalUnit_bijective line 414
  47. def OAI.Lech.NativeDescent.canonicalEquiv line 432