Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-11-15 16:09 3cd7b577

View on Github →

feat(data/(d)finsupp,fintype,fun_like): add fintype and (in)finite instances (#15725)

Estimated changes

Modified src/data/dfinsupp/basic.lean

added theorem dfinsupp.infinite_of_exists_right

added theorem dfinsupp.single_left_injective

Created src/data/finsupp/fintype.lean

Modified src/data/fintype/basic.lean

added theorem pi.infinite_of_exists_right

Created src/data/fun_like/fintype.lean

added theorem fun_like.finite'

added theorem fun_like.finite

Modified src/data/mv_polynomial/cardinal.lean