Commit 2024-10-16 02:20 9727486b

View on Github →

refactor: turn posPart into a notation class again (#17426)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Notation.lean

Modified Mathlib/Algebra/Order/Group/PosPart.lean

deleted def leOnePart

added theorem leOnePart_def

deleted def oneLePart

added theorem oneLePart_def

modified theorem oneLePart_mono

Modified Mathlib/Tactic/Positivity/Basic.lean

modified def Mathlib.Meta.Positivity.evalNegPart

modified def Mathlib.Meta.Positivity.evalPosPart

Modified Mathlib/Tactic/ToAdditive/Frontend.lean