Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-04-25 18:58 038f809c

View on Github →

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

Estimated changes