mathlib3

4ff8c3db - feat(analysis/normed_space/compact_operator): definition and basic facts about compact operators (#15467)