Commit 2025-08-16 14:23 200191bc

View on Github →

chore: more elementary Motzkin polynomial proof (#28482) In #23170 @Parcly-Taxel proved that the Motzkin polynomial over the reals is nonnegative. This PR switches the proof to a more elementary one that works over all linearly ordered commutative rings. Also move out of Analysis/MeanInequalities (since it no longer uses that tool).

Estimated changes

Modified Counterexamples.lean

Created Counterexamples/Motzkin.lean

added theorem motzkin_polynomial_nonneg

Modified Mathlib/Analysis/MeanInequalities.lean

deleted theorem Real.motzkin_polynomial_nonneg