OAI/RingTheory/Multiplicity/PrimitiveChartFaithfullyFlat.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Lech.PrimitiveChart.faithfullyFlat_away line 23
  2. abbrev OAI.Lech.BinaryChange.Binary line 73
  3. def OAI.Lech.BinaryChange.forward line 75
  4. def OAI.Lech.BinaryChange.backward line 79
  5. lemma OAI.Lech.BinaryChange.forward_backward line 83
  6. lemma OAI.Lech.BinaryChange.backward_forward line 88
  7. def OAI.Lech.BinaryChange.equiv line 93
  8. lemma OAI.Lech.BinaryChange.forward_homogeneous line 96
  9. def OAI.Lech.BinaryChange.transform line 108
  10. lemma OAI.Lech.BinaryChange.linear_degree line 111
  11. lemma OAI.Lech.BinaryChange.term_degree line 116
  12. lemma OAI.Lech.BinaryChange.transform_degree line 126
  13. lemma OAI.Lech.BinaryChange.term_coeff line 132
  14. lemma OAI.Lech.BinaryChange.transform_top line 144
  15. lemma OAI.Lech.BinaryChange.transform_eq_aeval line 151
  16. lemma OAI.Lech.BinaryChange.homogenize_transform line 161
  17. def OAI.Lech.BinaryChange.normalized line 172
  18. lemma OAI.Lech.BinaryChange.normalized_top line 175
  19. lemma OAI.Lech.BinaryChange.normalized_monic line 181
  20. lemma OAI.Lech.BinaryChange.normalized_degree line 188
  21. lemma OAI.Lech.BinaryChange.binary_factorization line 199
  22. lemma OAI.Lech.BinaryChange.factor_pair_unimodular line 230
  23. lemma OAI.Lech.BinaryCover.ordered_splitting_of_top line 245
  24. lemma OAI.Lech.BinaryCover.map_transform line 269
  25. lemma OAI.Lech.BinaryCover.map_normalized line 275
  26. structure OAI.Lech.BinaryCover.Data line 283
  27. theorem OAI.Lech.BinaryCover.exists_data line 300
  28. lemma OAI.Lech.RootTransitions.value_product line 357
  29. lemma OAI.Lech.RootTransitions.denominator_isUnit line 373
  30. lemma OAI.Lech.RootTransitions.linear_shift line 382
  31. lemma OAI.Lech.RootTransitions.normalized_shift line 391
  32. def OAI.Lech.RootGluing.rootShift line 420
  33. lemma OAI.Lech.RootGluing.map_inverse line 422
  34. lemma OAI.Lech.RootGluing.map_rootShift line 429
  35. lemma OAI.Lech.RootGluing.reverse_denominator line 435
  36. lemma OAI.Lech.RootGluing.rootShift_reverse line 443
  37. lemma OAI.Lech.RootGluing.normalized_shift line 451
  38. lemma OAI.Lech.RootGluing.denominator_comp line 462
  39. lemma OAI.Lech.RootGluing.rootShift_comp line 467
  40. lemma OAI.Lech.RootGluing.denominator_comp_isUnit line 481
  41. lemma OAI.Lech.RootGluing.mapped_factorization line 493
  42. lemma OAI.Lech.RootGluing.mapped_value line 500
  43. lemma OAI.Lech.RootGluing.denominator_unit line 506
  44. lemma OAI.Lech.RootGluing.shifted_factorization line 515
  45. def OAI.Lech.RootGluing.hom line 526
  46. lemma OAI.Lech.RootGluing.hom_root line 530
  47. lemma OAI.Lech.RootGluing.hom_comp line 535
  48. def OAI.Lech.RootGluing.equiv line 552
  49. lemma OAI.Lech.RootGluing.hom_cocycle line 557