Zulip Chat Archive

Stream: new members

Topic: rename cauchy schwartz?

view this post on Zulip 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 lemma inner_mul_le_inner_self.
Can I rename this?

Last updated: May 08 2021 at 05:14 UTC