Commit 2022-11-25 20:16 d04316c3

View on Github →

feat: port data.finite.defs (#698) Ports data.finite.defs with renaming to address Mathlib4 naming conventions Based on mathlib e50b8c261b0a000b806ec0e1356b41945eda61f7

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Finite/Defs.lean

added theorem Equiv.finite_iff

added theorem Equiv.infinite_iff

added theorem Finite.exists_equiv_fin

added theorem Finite.ofBijective

added theorem Finite.of_equiv

added theorem Function.Bijective.finite_iff

added theorem finite_iff_exists_equiv_fin

added theorem finite_or_infinite

added theorem not_finite

added theorem not_finite_iff_infinite

added theorem not_infinite_iff_finite