Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-05-19 00:34 cc74bcbd

View on Github →

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.

Estimated changes