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]
: