Mathlib v3 is deprecated. Go to Mathlib v4

Def continuous_linear_map.to_linear_map_ring_hom

Modification history

2022-05-19 00:34
src/topology/algebra/module/basic.lean
feat(topology/algebra/module/basic): add `continuous_linear_map.apply_module` (#14223) …
Added continuous_linear_map.to_linear_map_ring_homView on Github →