mathlib

dc985478 - feat(linear_algebra/projection): Extending maps from complement submodules to the entire module (#5981)

feat(linear_algebra/projection): Extending maps from complement submodules to the entire module (#5981) Given two linear maps from complement submodules, `of_is_comp` is the linear map extended to the entire module. This is useful whenever we would like to extend a linear map from a submodule to a map on the entire module.