Mathlib v3 is deprecated. Go to Mathlib v4

Def continuous_map.coe_fn_linear_map

Modification history

2021-05-30 04:33
src/topology/continuous_function/algebra.lean
feat(topology/continuous_function/algebra): add `coe_fn_(linear_map|ring_hom|alg_hom)` (#7720)
Added continuous_map.coe_fn_linear_mapView on Github →