Theorem Real.geom_mean_lt_arith_mean_weighted_iff_of_pos

Modification history

2024-12-02 01:32
Mathlib/Analysis/MeanInequalities.lean
feat: an equality condition for AM-GM inequality (#19435) …
Added Real.geom_mean_lt_arith_mean_weighted_iff_of_posView on Github →