Stream: new members
Topic: rename cauchy schwartz?
Chris M (Aug 16 2020 at 04:03):
The name of the cauchy schwartz inequality for real inner product spaces is
lemma inner_mul_inner_self_le (x y : F) : inner x y * inner x y ≤ inner x x * inner y y . It seems like it'd make more sense to call this
Can I rename this?
Last updated: May 08 2021 at 05:14 UTC