Mathlib v3 is deprecated. Go to Mathlib v4

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.

Estimated changes