Theorem Module.finrank_of_isLocalizedModule_of_free

Modification history

2024-11-25 08:40
Mathlib/RingTheory/LocalProperties/Projective.lean
feat: the free locus of a (finitely presented) module (#18691)
Added Module.finrank_of_isLocalizedModule_of_freeView on Github →