Theorem Module.length_eq_of_surjective

Modification history

2026-03-25 15:49
Mathlib/RingTheory/Length.lean
feat(RingTheory/Length): length of a module along a quotient map (#37126) …
Added Module.length_eq_of_surjectiveView on Github →