mathlib3
7fff35f5
- chore(algebra/pointwise): remove `@[simp]` from `singleton_one`/`singleton_zero` (#4592)
Go
Login via GitHub
Home
Pricing
FAQ
Install
Login
via GitHub
Commit
View On
GitHub
Commit
5 years ago
chore(algebra/pointwise): remove `@[simp]` from `singleton_one`/`singleton_zero` (#4592) This lemma simplified `{1}` and `{0}` to `1` and `0` making them unusable for other `singleton` lemmas.
References
#4925 - Make prime-avoidance branch build
Author
urkud
Parents
c9ae9e67
Loading