Def Mathlib.Meta.Positivity.evalAlgebraMap

Modification history

2025-11-19 06:07
Mathlib/Algebra/Order/Module/Algebra.lean
chore: move Mathlib to the module system (#31786) …
Deleted Mathlib.Meta.Positivity.evalAlgebraMapView on Github →
2024-01-30 18:04
Mathlib/Algebra/Order/Module/Algebra.lean
feat: `positivity` extension for `algebraMap` (#9961)
Added Mathlib.Meta.Positivity.evalAlgebraMapView on Github →