Mathlib v3 is deprecated. Go to Mathlib v4

Theorem submodule.ker_subtypeL

Modification history

2022-09-27 09:35
src/topology/algebra/module/basic.lean
chore(topology/algebra/module/basic): remove `continuous_linear_map.ker` and `continuous_linear_map.range` (#16208) …
Modified submodule.ker_subtypeLView on Github →
2022-07-28 02:26
src/analysis/normed_space/linear_isometry.lean
chore(topology/algebra/module, analysis/normed_space/linear_isometry): dedup `submodule.subtypeL` and `continuous_linear_map.subtype_val` (#15700) …
Modified submodule.ker_subtypeLView on Github →
2021-04-10 08:01
src/analysis/normed_space/linear_isometry.lean
feat(analysis/normed_space/banach): a range with closed complement is itself closed (#6972) …
Added submodule.ker_subtypeLView on Github →