Commit 2020-05-25 12:50 3e0668e0
View on Github →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