mathlib
b1269b0d
- chore(algebra/order/ring): add a few aliases (#11911)
Go
Login via GitHub
Home
Pricing
FAQ
Install
Login
via GitHub
Commit
View On
GitHub
Commit
3 years ago
chore(algebra/order/ring): add a few aliases (#11911) Add aliases `one_pos`, `two_pos`, `three_pos`, and `four_pos`. We used to have (some of) these lemmas. They were removed during one of cleanups but it doesn't hurt to have aliases.
References
lean-3.39.0
Author
urkud
Parents
85d9f218
Loading