Commit 2021-12-08 03:50 2bfa7684

View on Github →

feat(analysis/normed_space/operator_norm): module and norm instances on continuous semilinear maps (#10494) This PR adds a module and a norm instance on continuous semilinear maps, generalizes most of the results in operator_norm.lean to the semilinear case. Many of these results require the ring homomorphism to be isometric, which is expressed via the new typeclass [ring_hom_isometric σ].

Estimated changes

modified theorem continuous_linear_map.bound
modified theorem linear_map.bound_of_shell
modified theorem norm_image_of_norm_zero