Commit 2022-11-27 08:50 7c09b053

View on Github →

feat: port Data.Countable.Defs (#736) Mathlib SHA: 71ca477041bcd6d7c745fe555dc49735c12944b7

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Countable/Defs.lean

added theorem Countable.exists_injective_nat

added theorem Countable.of_equiv

added theorem Equiv.countable_iff

added theorem countable_iff_exists_surjective

added theorem exists_surjective_nat