[Merged by Bors] - feat(LinearAlgebra/Projection): add quotientEquivOfIsCompl_comp_mkQ and quotientEquivOfIsTopCompl_comp_mkQ#39613

sharky564 wants to merge 9 commits into

leanprover-community:masterleanprover-community/mathlib4:masterfrom

sharky564:SK_quotientEquiv_comp_mkQsharky564/mathlib4:SK_quotientEquiv_comp_mkQCopy head branch name to clipboard