mathlib
cc74bcbd - feat(topology/algebra/module/basic): add `continuous_linear_map.apply_module` (#14223)

Commit
3 years ago
feat(topology/algebra/module/basic): add `continuous_linear_map.apply_module` (#14223) This matches `linear_map.apply_module`, but additionally provides `has_continuous_const_smul`. This also adds the missing `continuous_linear_map.semiring` and `continuous_linear_map.monoid_with_zero` instances.
Author
Parents
Loading