Commit 2023-02-15 14:31 12bf962c

View on Github →

feat: port Data.Fintype.CardEmbedding (#2166)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Fintype/CardEmbedding.lean

added theorem Fintype.card_embedding_eq

added theorem Fintype.card_embedding_eq_of_infinite

added theorem Fintype.card_embedding_eq_of_unique

Modified Mathlib/Data/Fintype/Pi.lean