Commit 2024-10-18 19:09 7d20facb

View on Github →

feat: variant of the binary AM-GM inequality (#17877) added variant of binary AM-GM inequality

Estimated changes

Modified Mathlib/Algebra/Order/Ring/Unbundled/Basic.lean

added theorem four_mul_le_sq_add

Modified Mathlib/Data/Nat/Cast/Defs.lean

added theorem two_add_two_eq_four