mathlib3

49f8b6b8 - chore(analysis/mean_inequalities[_pow]): use vector notation (#10546)

chore(analysis/mean_inequalities[_pow]): use vector notation (#10546) Several elementary inequalities in the library are expressed both in arbitrary n-ary versions and in explicit binary, ternary etc versions, with the latter deduced from the former. This PR introduces vector notation to the proof terms deducing the latter from the former, which shortens them, and also makes them more readable.