Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-05-27 18:15 4c1a8268

View on Github →

refactor(data/set/finite): use hypotheses for fintype assumptions in simp rules

Estimated changes

modified theorem set.card_insert
added theorem set.empty_card'
modified theorem set.empty_card