Theorem IsCompactOperator.sub

Modification history

2023-05-09 23:59

Mathlib/Analysis/NormedSpace/CompactOperator.lean

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

Added IsCompactOperator.sub View on Github →