Theorem IsCompactOperator.neg

Modification history

2023-05-09 23:59

Mathlib/Analysis/NormedSpace/CompactOperator.lean

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

Added IsCompactOperator.neg View on Github →