Commit 2025-04-04 14:05 66693aea

View on Github →

feat(RingTheory): lengths of modules (#23663)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Module/Submodule/Map.lean

added theorem Submodule.comap_lt_of_lt_map_of_injective

added theorem Submodule.map_covBy_of_injective

added theorem Submodule.map_lt_map_iff_of_injective

Modified Mathlib/LinearAlgebra/Span/Basic.lean

added theorem Submodule.comap_covBy_of_surjective

Modified Mathlib/Order/Atoms.lean

Modified Mathlib/Order/KrullDimension.lean

added theorem Order.krullDim_eq_one_iff_of_boundedOrder

Modified Mathlib/Order/RelSeries.lean

added theorem LTSeries.exists_relSeries_covBy_and_head_eq_bot_and_last_eq_bot

Modified Mathlib/RingTheory/FiniteLength.lean

added theorem IsFiniteLength.of_injective

added theorem IsFiniteLength.of_surjective

Created Mathlib/RingTheory/Length.lean

added theorem Module.coe_length

added def Module.length

added theorem Module.length_compositionSeries

added theorem Module.length_eq_add_of_exact

added theorem Module.length_eq_coheight

added theorem Module.length_eq_height

added theorem Module.length_eq_zero

added theorem Module.length_eq_zero_iff

added theorem Module.length_ne_top

added theorem Module.length_ne_top_iff

added theorem Module.length_pos

added theorem Module.length_pos_iff