mathlib3

1a438889 - feat(analysis/normed_space/operator_norm): bundle more arguments (#6207)

feat(analysis/normed_space/operator_norm): bundle more arguments (#6207) * Drop `lmul_left` in favor of a partially applied `lmul`. * Use `lmul_left_right` in `has_fderiv_at_ring_inverse` and related lemmas. * Add bundled `compL`, `lmulₗᵢ`, `lsmul`. * Make `𝕜` argument in `of_homothety` implicit. * Add `deriv₂` and `bilinear_comp`. Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>