Commit 2025-01-08 16:29 a2cbb66e

View on Github →

feat(Topology/Algebra) finite modules over compact rings are compact (#20291)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/Algebra/Module/Compact.lean

added theorem Ideal.isCompact_of_fg

added theorem Module.Finite.compactSpace

added theorem Submodule.isCompact_of_fg