Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-11-06 07:48 614849cd

View on Github →

feat(data/fintype/basic): a type is infinite if it admits an injective map to a proper subset (#17204)

Estimated changes