mathlib icon indicating copy to clipboard operation
mathlib copied to clipboard
verified publisher icon leanprover-community

chore(algebra/order/monoid_lemmas_zero_lt): use suffix `ₚ`, create aliases

Open astrainfinita opened this issue 3 years ago • 1 comments

The second part of #16449

This PR uses the suffix "ₚ" on some lemmas which assume positivity. Due to name conflicts, these similar lemmas have dissimilar names currently.

If there is a better way to resolve name conflicts, please feel free to comment.

  • [x] depends on: #16480

Open in Gitpod

astrainfinita avatar Sep 15 '22 13:09 astrainfinita

This PR/issue depends on:

  • ~~leanprover-community/mathlib#16480~~ By Dependent Issues (🤖). Happy coding!

mathlib-dependent-issues-bot avatar Sep 16 '22 10:09 mathlib-dependent-issues-bot

Note that this file has now been ported to mathlib4, so will need a synchronization PR.

kim-em avatar Nov 18 '22 04:11 kim-em

This was forward-ported as https://github.com/leanprover-community/mathlib4/pull/9249 (and ultimately abandoned there)

eric-wieser avatar Mar 23 '24 23:03 eric-wieser