Commit 2024-11-23 14:58 6343082c

feat: Sedrakyan's lemma (#19311) This is a specialization of the Cauchy-Schwarz inequality which is often useful in math olympiad problems. In order to prove it in general ordered semifields, we have to show slightly more general forms of the AM-GM and Cauchy-Schwarz inequalities, which indirectly work with square roots.