operator_norm): remove an import to data.equiv.transfer_instance (#10094)

Commit

4 years ago

chore(analysis/normed_space/operator_norm): remove an import to data.equiv.transfer_instance (#10094) This import isn't needed, and the spelling without it is shorter.

Author

eric-wieser

Parents

0144b6ca

mathlib3 b1d5446e - chore(analysis/normed_space/operator_norm): remove an import to data.equiv.transfer_instance (#10094)

mathlib3
b1d5446e - chore(analysis/normed_space/operator_norm): remove an import to data.equiv.transfer_instance (#10094)