Commit 2021-02-16 12:05 1a438889

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.