mathlib

0744a3a9 - feat(analysis/normed_space/operator_norm): extension of a uniform continuous function (#1649)

feat(analysis/normed_space/operator_norm): extension of a uniform continuous function (#1649) * Extension of a uniform continuous function * Use characteristic properties of an extended function, instead of the explicit construction * Add documentation on similar results in the library * Update src/topology/algebra/uniform_extension.lean Co-Authored-By: sgouezel <sebastien.gouezel@univ-rennes1.fr> * Travis failed for no reason * Update uniform_extension.lean * eliminate `uniform_extension.lean` * Update operator_norm.lean * Update operator_norm.lean * Remove `M` * Fix docstring; extend_zero should be a simp lemma