Commit 2020-10-13 06:30 7fff35f5
View on Github →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.
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.