feat(Analysis/InnerProductSpace): singleton basis for 1d space#37506

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

wwylele:orth-basis-singlewwylele/mathlib4:orth-basis-singleCopy head branch name to clipboard