mathlib
cad19073 - chore(topology/algebra/module, analysis/normed_space/linear_isometry): dedup `submodule.subtypeL` and `continuous_linear_map.subtype_val` (#15700)

Commit
2 years ago
chore(topology/algebra/module, analysis/normed_space/linear_isometry): dedup `submodule.subtypeL` and `continuous_linear_map.subtype_val` (#15700) To designate the continuous linear inclusion of a submodule into the ambient space, we currently have both `continuous_linear_map.subtype_val` (correct assumptions, name not consistent with `submodule.subtype`) and `submodule.subtypeL` (good name, but way too strong assumptions). This keeps the best of both worlds.
Author
Parents
  • src
    • analysis
      • calculus
        • implicit.lean
      • normed_space
        • complemented.lean
        • linear_isometry.lean
    • topology/algebra/module
      • basic.lean