Commit 2021-12-30 14:54 f6d0f8d1

View on Github →

refactor(analysis/normed_space/operator_norm): split a proof (#11112) Split the proof of continuous_linear_map.complete_space into reusable steps. Motivated by #9862

Estimated changes