operator_norm): bundle another argument into the homs (#5899)

Commit

4 years ago

chore(linear_algebra/basic, analysis/normed_space/operator_norm): bundle another argument into the homs (#5899) Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>

Author

eric-wieser

Parents

7f11d721

mathlib3 117e7290 - chore(linear_algebra/basic, analysis/normed_space/operator_norm): bundle another argument into the homs (#5899)

mathlib3
117e7290 - chore(linear_algebra/basic, analysis/normed_space/operator_norm): bundle another argument into the homs (#5899)