Commit 2024-10-08 18:55 0d4b02ed

View on Github →

fix(Group/PosPart): fix multiplicative version (#17540) These lemmas were incorrectly stated with the multiplicative version, and so had two identical forms, both additive. This PR restores the multiplicative version, and also generalises.

Estimated changes

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

modified theorem Pi.leOnePart_apply

modified theorem Pi.leOnePart_def

modified theorem Pi.oneLePart_apply

modified theorem Pi.oneLePart_def