mathlib
3875012a - feat(data/quot): add `map'`, `hrec_on'`, and `hrec_on₂'` (#3148)

Commit

5 years ago

feat(data/quot): add `map'`, `hrec_on'`, and `hrec_on₂'` (#3148) Also add a few `simp` lemmas

Author

urkud

Parents