mathlib
6548be43
- chore(data/quot): Add missing simp lemmas (#5372)
Go
Login via GitHub
Home
Pricing
FAQ
Install
Login
via GitHub
Commit
View On
GitHub
Commit
5 years ago
chore(data/quot): Add missing simp lemmas (#5372) These are called `lift_on'_beta` for consistency with `lift_on_beta`; even though we also have `map_mk'` etc in the same file.
Author
eric-wieser
Parents
78940f46
Loading