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

Commit

3 years ago

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

Author

urkud

Parents