Theorems · Theorem · functional analysis

isModuleTopologyOfFiniteDimensional

∀ {𝕜 : Type u} [hnorm : NontriviallyNormedField 𝕜] {E : Type v} [inst : AddCommGroup E] [inst_1 : Module 𝕜 E]
  [inst_2 : TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E] [CompleteSpace 𝕜] [T2Space E]
  [FiniteDimensional 𝕜 E], IsModuleTopology 𝕜 E

A finite-dimensional t2 vector space over a complete field must carry the module topology. Not declared as a global instance only for performance reasons.

Defined in

Mathlib.Topology.Algebra.Module.FiniteDimension

Cited by

0 results in Mathlib

Foundations

Depth 166 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NontriviallyNormedFieldAddCommGroupModuleTopologicalSpaceIsTopologicalAddGroupContinuousSMulCompleteSpaceT2SpaceFiniteDimensional