mathlib

3e0668e0 - feat(linear_algebra/projection): add `equiv_prod_of_surjective_of_is_compl` (#2787)

feat(linear_algebra/projection): add `equiv_prod_of_surjective_of_is_compl` (#2787) If kernels of two surjective linear maps `f`, `g` are complement subspaces, then `x ↦ (f x, g x)` defines a linear equivalence. I also add a version of this equivalence for continuous maps. Depends on #2785