Def Mathlib.Meta.Positivity.evalHSMul

Modification history

2025-09-06 04:27
Mathlib/Algebra/Order/Module/Field.lean
chore: deprecate `OrderedSMul` (#28817) …
Deleted Mathlib.Meta.Positivity.evalHSMulView on Github →
2025-06-18 15:21
Mathlib/Algebra/Order/Module/Defs.lean
chore(Algebra/Order/Module/Defs): don't import fields (#25584) …
Modified Mathlib.Meta.Positivity.evalHSMulView on Github →
2023-12-23 10:52
Mathlib/Algebra/Order/Module/Defs.lean
refactor: Deduplicate monotonicity of `•` lemmas (#9179) …
Modified Mathlib.Meta.Positivity.evalHSMulView on Github →
2023-11-09 15:38
Mathlib/Algebra/Order/SMul.lean
feat: port smul positivity extension (#8067)
Added Mathlib.Meta.Positivity.evalHSMulView on Github →