Commit 2023-07-14 07:29 36eb6512

View on Github →

feat: port Analysis.InnerProductSpace.OfNorm (#5885)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/InnerProductSpace/OfNorm.lean

added theorem Continuous.inner_

added theorem InnerProductSpace.toInnerProductSpaceable

added theorem InnerProductSpaceable.Inner_.conj_symm

added theorem InnerProductSpaceable.Inner_.norm_sq

added theorem InnerProductSpaceable.add_left

added theorem InnerProductSpaceable.innerProp

added theorem InnerProductSpaceable.innerProp_neg_one

added theorem InnerProductSpaceable.nat

added theorem nonempty_innerProductSpace