Theorem IsLocalizedModule.of_exists_mul_mem

Modification history

2024-11-25 08:40
Mathlib/Algebra/Module/LocalizedModule/Basic.lean
feat: the free locus of a (finitely presented) module (#18691)
Added IsLocalizedModule.of_exists_mul_memView on Github →