PR#19435 (equality condition for AM-GM inequality)

Stream: mathlib4

[Zhu]

I have submitted a PR mathlib4#19435 to Mathlib4 that provides the equality condition for the weighted version of the AM-GM inequality. I am currently working on completing the equality conditions for other cases as well.

Since this is my first PR to Mathlib4, I wanted to ask whether it is appropriate for inclusion and if there are any improvements I should make.

Any feedback or suggestions would be greatly appreciated.
Thank you for your time! :smiley: