OAI/RingTheory/Multiplicity/RootTowerLengthEq.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.Lech.RootTower.length_eq_of_residue_surjective line 20
  2. lemma OAI.Lech.RootTower.normalizedLength_stage_quotient line 40
  3. lemma OAI.Lech.RootTower.rootMap_pow line 73
  4. def OAI.Lech.RootTower.perfectMap line 78
  5. lemma OAI.Lech.RootTower.perfectMap_root line 81
  6. lemma OAI.Lech.RootTower.perfectMap_injective line 87
  7. instance OAI.Lech.RootTower.perfectDomain line 105
  8. instance OAI.Lech.RootTower.perfectFractionAlgebra line 109
  9. instance OAI.Lech.RootTower.perfectFraction line 112
  10. instance OAI.Lech.RootTower.perfectAlgebra line 125
  11. instance OAI.Lech.RootTower.perfectIntegral line 127
  12. instance OAI.Lech.RootTower.perfectNormal line 134
  13. instance OAI.Lech.RootTower.perfectBaseAlgebra line 167
  14. instance OAI.Lech.RootTower.perfectBaseTower line 170
  15. instance OAI.Lech.RootTower.perfectExtensionTower line 173
  16. def OAI.Lech.RootTower.perfectOf line 176
  17. lemma OAI.Lech.RootTower.perfect_span line 180
  18. lemma OAI.Lech.RootTower.perfect_basis_independent line 218
  19. lemma OAI.Lech.RootTower.perfect_basis_span line 234
  20. def OAI.Lech.RootTower.perfectBasis line 248
  21. lemma OAI.Lech.RootTower.perfectBasis_apply line 252
  22. instance OAI.Lech.RootTower.perfectExtensionFinite line 257
  23. lemma OAI.Lech.TraceConductor.finite_denominators line 270
  24. theorem OAI.Lech.TraceConductor.exists_conductor line 299
  25. lemma OAI.Lech.TraceConductor.denominator_of_span line 328
  26. lemma OAI.Lech.TraceConductor.denominator_fraction line 362
  27. lemma OAI.Lech.RootTower.perfectMap_comp line 381
  28. lemma OAI.Lech.RootTower.perfectMap_of line 390
  29. instance OAI.Lech.RootTower.perfectOriginalAlgebra line 401
  30. instance OAI.Lech.RootTower.perfectOriginalTower line 403
  31. instance OAI.Lech.RootTower.perfectOriginalRootTower line 405
  32. instance OAI.Lech.RootTower.perfectScalarTower line 409
  33. def OAI.Lech.TraceConductor.perfectOrder line 430
  34. theorem OAI.Lech.TraceConductor.exists_perfect_conductor line 436