Mathlib v3 is deprecated. Go to Mathlib v4

Theorem continuous_linear_map.to_linear_map_eq_coe

Modification history

2021-10-05 08:58
src/topology/algebra/module.lean
refactor(topology/algebra/module): continuous semilinear maps (#9539) …
Modified continuous_linear_map.to_linear_map_eq_coeView on Github →
2021-06-25 10:35
src/topology/algebra/module.lean
chore(data/complex/{module, is_R_or_C}, analysis/complex/basic): rationalize the structure provided for `conj` and `of_real` (#8014) …
Added continuous_linear_map.to_linear_map_eq_coeView on Github →