feat(Analysis/InnerProductSpace): generalized determinant of a rectangle matrix / linear map#37295

wwylele wants to merge 4 commits intoleanprover-community:masterleanprover-community/mathlib4:masterfrom

wwylele:norm-detwwylele/mathlib4:norm-detCopy head branch name to clipboard