Theorems · Theorem · functional analysis

Module.Finite.compactSpace

∀ (R : Type u_1) (M : Type u_2) [inst : CommSemiring R] [inst_1 : TopologicalSpace R] [inst_2 : AddCommMonoid M]
  [inst_3 : Module R M] [inst_4 : TopologicalSpace M] [ContinuousAdd M] [ContinuousSMul R M] [CompactSpace R]
  [Module.Finite R M], CompactSpace M

Defined in: Mathlib.Topology.Algebra.Module.Compact
Cited by: 0 results in Mathlib
Foundations: Depth 84 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: CommSemiring TopologicalSpace AddCommMonoid Module TopologicalSpace ContinuousAdd ContinuousSMul CompactSpace Module.Finite

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites10

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

TopologicalSpacestatement and proof · cited by 24,529
Modulestatement and proof · cited by 20,661
AddCommMonoidstatement and proof · cited by 12,281
CommSemiringstatement and proof · cited by 10,911
Module.Finitestatement and proof · cited by 1,032
ContinuousSMulstatement and proof · cited by 1,016
ContinuousAddstatement and proof · cited by 777
CompactSpacestatement and proof · cited by 593
Module.Finite.fg_topproof · cited by 28
Submodule.isCompact_of_fgproof · cited by 2

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.