Def continuous_map.coe_fn_ring_hom

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_ring_homView on Github →