Compact submodules

theorem Submodule.isCompact_of_fg {R : Type u_1} {M : Type u_2} [CommSemiring R] [TopologicalSpace R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [ContinuousAdd M] [ContinuousSMul R M] [CompactSpace R] {N : Submodule R M} (hN : N.FG) : IsCompact ↑N

theorem Ideal.isCompact_of_fg {R : Type u_1} [CommSemiring R] [TopologicalSpace R] [IsTopologicalSemiring R] [CompactSpace R] {I : Ideal R} (hI : I.FG) : IsCompact ↑I

theorem Module.Finite.compactSpace (R : Type u_1) (M : Type u_2) [CommSemiring R] [TopologicalSpace R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [ContinuousAdd M] [ContinuousSMul R M] [CompactSpace R] [Module.Finite R M] : CompactSpace M

@[instance 100]

instance IsNoetherianRing.isClosed_ideal {R : Type u_3} [CommRing R] [TopologicalSpace R] [IsTopologicalRing R] [IsNoetherianRing R] [CompactSpace R] [T2Space R] (I : Ideal R) : IsClosed ↑I