Theorem Real.motzkin_polynomial_nonneg

Modification history

2025-08-16 14:23
Mathlib/Analysis/MeanInequalities.lean
chore: more elementary Motzkin polynomial proof (#28482) …
Deleted Real.motzkin_polynomial_nonnegView on Github →
2025-03-21 06:55
Mathlib/Analysis/MeanInequalities.lean
feat: the Motzkin polynomial is nonnegative (#23170) …
Added Real.motzkin_polynomial_nonnegView on Github →