Mathlib v3 is deprecated. Go to Mathlib v4

Theorem continuous_linear_map.coe_fn_injective

Modification history

2021-10-05 08:58
src/topology/algebra/module.lean
refactor(topology/algebra/module): continuous semilinear maps (#9539) …
Modified continuous_linear_map.coe_fn_injectiveView on Github →
2021-07-22 14:12
src/topology/algebra/module.lean
chore(*): Prevent lemmas about the injectivity of `coe_fn` introducing un-reduced lambda terms (#8386) …
Modified continuous_linear_map.coe_fn_injectiveView on Github →
2021-03-18 19:27
src/topology/algebra/module.lean
chore(*): update `injective` lemma names to match the naming guide (#6740) …
Added continuous_linear_map.coe_fn_injectiveView on Github →
2020-10-20 10:23
src/topology/algebra/module.lean
chore(*): review some lemmas about injectivity of coercions (#4711) …
Deleted continuous_linear_map.coe_fn_injectiveView on Github →
2020-10-08 15:41
src/topology/algebra/module.lean
chore(*): add a few more `unique` instances (#4511) …
Added continuous_linear_map.coe_fn_injectiveView on Github →