Theorem Submodule.isCompact_of_fg

Modification history

2025-01-08 16:29
Mathlib/Topology/Algebra/Module/Compact.lean
feat(Topology/Algebra) finite modules over compact rings are compact (#20291)
Added Submodule.isCompact_of_fgView on Github →