Mathlib v3 is deprecated. Go to Mathlib v4

Def equiv.embedding_congr

Modification history

2021-05-21 11:28

src/logic/embedding.lean

feat(data/fintype/card_embedding): the birthday problem (#7363)

Added equiv.embedding_congr View on Github →