diff --git a/Mathlib/Data/Fintype/Card.lean b/Mathlib/Data/Fintype/Card.lean index 920d796fed357..764b002919793 100644 --- a/Mathlib/Data/Fintype/Card.lean +++ b/Mathlib/Data/Fintype/Card.lean @@ -42,7 +42,7 @@ See `Infinite.of_injective` and `Infinite.of_surjective`. ## Instances We provide `Infinite` instances for -* specific types: `ℕ`, `ℤ` +* specific types: `ℕ`, `ℤ`, `String` * type constructors: `Multiset α`, `List α` -/ @@ -1039,6 +1039,12 @@ instance [Nonempty α] : Infinite (Multiset α) := instance [Nonempty α] : Infinite (List α) := Infinite.of_surjective ((↑) : List α → Multiset α) (surjective_quot_mk _) +instance String.infinite : Infinite String := + Infinite.of_injective (String.mk) <| by + intro _ _ h + cases h with + | refl => rfl + instance Infinite.set [Infinite α] : Infinite (Set α) := Infinite.of_injective singleton Set.singleton_injective #align infinite.set Infinite.set