Add some helpers in Hom.lean, address TODOs in GramSchmidtOrtho.lean#6

michaellee94 wants to merge 2 commits intogrunweg:gramSchmidt-sections-smoothgrunweg/mathlib4:gramSchmidt-sections-smoothfrom

michaellee94:michaellee94/gramSchmidt-sections-smoothmichaellee94/mathlib4:michaellee94/gramSchmidt-sections-smoothCopy head branch name to clipboard