chore: fix docstring (#6012)

leanprover-community · Jul 20, 2023 · 852259c · 852259c
1 parent 5070d54
commit 852259c
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/Mathlib/Data/Set/Finite.lean b/Mathlib/Data/Set/Finite.lean
@@ -20,7 +20,7 @@ about finite sets and gives ways to manipulate `Set.Finite` expressions.
 
 * `Set.Finite : Set α → Prop`
 * `Set.Infinite : Set α → Prop`
-* `Set.to_finite` to prove `Set.Finite` for a `Set` from a `Finite` instance.
+* `Set.toFinite` to prove `Set.Finite` for a `Set` from a `Finite` instance.
 * `Set.Finite.toFinset` to noncomputably produce a `Finset` from a `Set.Finite` proof.
   (See `Set.toFinset` for a computable version.)