Theorem IsCompactOperator.restrict

Modification history

2023-05-09 23:59

Mathlib/Analysis/NormedSpace/CompactOperator.lean

feat: port Analysis.NormedSpace.CompactOperator (#3805)

Added IsCompactOperator.restrict View on Github →