Commit 2024-09-05 10:13 f9affb42

View on Github →

feat(KrullDimension): height refactor, initial stuff (#16480) This refactors and extends the definition of height. Notable changes:

  • Everything put into namespace Order
  • Type of krullDim changed from WithBot (WithTop Nat) to WithBot ENat.
  • Type of height changed from WithBot (WithTop Nat) to ENat.
  • Definition of height via LTSeries rather than krullDim From the Carleson project.

Estimated changes

added theorem Order.height_le
added theorem Order.height_mono
added theorem Order.length_le_height
deleted theorem height_mono
deleted theorem krullDim_eq_iSup_height
deleted theorem krullDim_eq_of_orderIso
deleted theorem krullDim_le_of_strictMono
deleted theorem krullDim_orderDual