Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-04-12 15:23 2af01474

View on Github →

chore(data/equiv/basic): add simps attribute to some defs (#7137)

Estimated changes

modified def equiv.empty_sum
modified def equiv.pempty_sum
modified def equiv.sum_empty
modified def equiv.sum_pempty