mathlib
4fe734da
- fix(algebra/indicator_function): add missing decidable instances to lemma statements (#13834)
Go
Login via GitHub
Home
Pricing
FAQ
Install
Login
via GitHub
Commit
View On
GitHub
Commit
3 years ago
fix(algebra/indicator_function): add missing decidable instances to lemma statements (#13834) This keeps the definition of `set.indicator` as non-computable, but ensures that when lemmas are applied they generalize to any decidable instances.
Author
eric-wieser
Parents
cf5fa84c
Loading