Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-07-21 17:32 ae1c7eef

View on Github →

docs(analysis/normed_space/bounded_linear_map): add module docstring (#8263)

Estimated changes

Modified src/analysis/normed_space/bounded_linear_maps.lean

modified theorem continuous_linear_map.is_bounded_linear_map_comp_left

modified theorem continuous_linear_map.is_bounded_linear_map_comp_right

modified def is_bounded_bilinear_map.deriv