mathlib3

d3d37017 - feat(analysis/mean_inequalities): AM and GM are equal on a constant tuple (#12179)

feat(analysis/mean_inequalities): AM and GM are equal on a constant tuple (#12179) The converse is also true, but I have not gotten around to proving it. Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>