Theorem isCompactOperator_id_iff_finiteDimensional

Modification history

2026-02-18 19:37
Mathlib/Analysis/Normed/Module/FiniteDimension.lean
feat(Analysis/Normed/Operator/Compact): criteria for compactness of the identity operator (#35196) …
Added isCompactOperator_id_iff_finiteDimensionalView on Github →