mathlib
7d7e850b
- chore(category_theory/sites): nicer names (#4816)
Go
Login via GitHub
Home
Pricing
FAQ
Install
Login
via GitHub
Commit
View On
GitHub
Commit
5 years ago
chore(category_theory/sites): nicer names (#4816) Changes the name `arrows_with_codomain` to `presieve` which is more suggestive and shorter, and changes `singleton_arrow` to `singleton`, since it's in the presieve namespace anyway.
References
#4925 - Make prime-avoidance branch build
Author
b-mehta
Parents
8b858d0b
Loading