Theorem Real.geom_mean_eq_arith_mean_weighted_iff

Modification history

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