Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-01 01:14 540fb943

View on Github →

feat(data/fintype/basic): bijection preserves cardinality (#9473) We don't seem to have this lemma yet, so I've added it.

Estimated changes