Commit 2025-04-05 11:36 97a74038

View on Github →

feat(RingTheory): length of submodules and quotients (#23679)

Estimated changes

Modified Mathlib/LinearAlgebra/Quotient/Basic.lean

modified def Submodule.comapMkQRelIso

Modified Mathlib/RingTheory/Length.lean

added theorem LinearEquiv.length_eq

added theorem Module.length_bot

added theorem Module.length_le_of_injective

added theorem Module.length_le_of_surjective

added theorem Module.length_quotient

added theorem Module.length_submodule

added theorem Module.length_top