rename cauchy schwartz?

Stream: new members

[Chris M]

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?