[Merged by Bors] - feat(Analysis/InnerProductSpace): inner products on exterior powers#40724

justus-springer wants to merge 20 commits into

leanprover-community:masterleanprover-community/mathlib4:masterfrom

justus-springer:justus/exterior-power-inner-productjustus-springer/mathlib4:justus/exterior-power-inner-productCopy head branch name to clipboard