Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-02-10 15:17 7fd4dcf1

View on Github →

feat(analysis/normed_space/operator_norm): bundle more arguments (#6140)

  • bundle the first argument of continuous_linear_map.smul_rightL;
  • add continuous_linear_map.flip and continuous_linear_map.flipₗᵢ;
  • use flip to redefine apply.

Estimated changes