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.