Mathlib v3 is deprecated. Go to Mathlib v4

Theorem mul_inv_eq'

Modification history

2019-04-25 18:58
src/analysis/normed_space/bounded_linear_maps.lean
refactor(analysis/normed_space/operator_norm): replace subspace with … (#955) …
Deleted mul_inv_eq'View on Github →
2018-08-29 14:48
analysis/bounded_linear_maps.lean
cleanup(analysis/bounded_linear_maps): some reorganization
Added mul_inv_eq'View on Github →