Theorem IsCompactOperator.sub

Modification history

2025-02-16 15:19
Mathlib/Analysis/Normed/Operator/Compact.lean
chore: rename Topological(Semi)Ring -> IsTopological(Semi)Ring and Topological(Add)Group -> IsTopological(Add)Group (#21472)
Modified IsCompactOperator.subView on Github →
2023-05-09 23:59
Mathlib/Analysis/NormedSpace/CompactOperator.lean
feat: port Analysis.NormedSpace.CompactOperator (#3805)
Added IsCompactOperator.subView on Github →