mathlib3
bfb15ebd - chore(analysis/normed_space/operator_norm): add missing lemma (#17449)

Commit

3 years ago

chore(analysis/normed_space/operator_norm): add missing lemma (#17449)

Author

mcdoll

mcdoll

Parents

Loading