Theorem Ideal.isCompact_of_fg

Modification history

2025-02-16 15:19
Mathlib/Topology/Algebra/Module/Compact.lean
chore: rename Topological(Semi)Ring -> IsTopological(Semi)Ring and Topological(Add)Group -> IsTopological(Add)Group (#21472)
Modified Ideal.isCompact_of_fgView on Github →
2025-01-08 16:29
Mathlib/Topology/Algebra/Module/Compact.lean
feat(Topology/Algebra) finite modules over compact rings are compact (#20291)
Added Ideal.isCompact_of_fgView on Github →