mathlib
d04429fa
- chore(logic/embedding,order/order_iso): review (#2618)
Go
Login via GitHub
Home
Pricing
FAQ
Install
Login
via GitHub
Commit
View On
GitHub
Commit
6 years ago
chore(logic/embedding,order/order_iso): review (#2618) * swap `inj` with `inj'` to match other bundled homomorphisms; * make some arguments explicit to avoid `embedding.of_surjective _` in the pretty printer output; * make `set_value` computable.
References
#2700 - Fix merge conflict
Author
urkud
Parents
08d43163
Loading