mathlib3

038f809c - refactor(analysis/normed_space/operator_norm): replace subspace with … (#955)

refactor(analysis/normed_space/operator_norm): replace subspace with … (#955) * refactor(analysis/normed_space/operator_norm): replace subspace with structure * refactor(analysis/normed_space/operator_norm): add coercions