Commit 2024-08-07 01:32 af4fabaf

feat(Analysis/InnerProductSpace/Basic): add PreInnerProductSpace (#14024) add the structure PreInnerProductSpace, which does not assume definite for the inner product, with a proof of the Cauchy-Schwarz inequality using the discriminant. Motivation: Such structures arise very often in applications, and by quotienting the kernel one obtains InnerProductSpace.Core. I duplicated most of the proofs from the namespace InnerProductSpace.Core and put them under the namespace PreInnerProductSpace . Is there a better way?