Theorem isNormableSpace_of_finiteDimensional

Modification history

2026-09-29 15:02
Mathlib/Topology/Algebra/Module/FiniteDimension.lean
feat: introduce an IsNormableSpace class (#42983) …
Added isNormableSpace_of_finiteDimensionalView on Github →