Commit 2026-03-25 15:49 ec3a721d
View on Github →feat(RingTheory/Length): length of a module along a quotient map (#37126) This PR proves that the length of a module doesn't change along a quotient map.
feat(RingTheory/Length): length of a module along a quotient map (#37126) This PR proves that the length of a module doesn't change along a quotient map.