docs(FunLike/Fintype): fix typo in doc comments (#11402)

The non-dependent version of `DFunLike.{fintype,finite}` is called `FunLike.{fintype,finite}`; the names in the docstring do not exist.
leanprover-community · Mar 16, 2024 · 14b7f74 · 14b7f74
1 parent a81a438
commit 14b7f74
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/Mathlib/Data/FunLike/Fintype.lean b/Mathlib/Data/FunLike/Fintype.lean
@@ -19,8 +19,8 @@ This corresponds to the following two pairs of declarations:
    codomain are.
  * `DFunLike.finite` is a lemma stating all `DFunLike`s are finite if their domain and
    codomain are.
- * `DFunLike.fintype'` is a non-dependent version of `DFunLike.fintype` and
- * `DFunLike.finite` is a non-dependent version of `DFunLike.finite`, because dependent instances
+ * `FunLike.fintype` is a non-dependent version of `DFunLike.fintype` and
+ * `FunLike.finite` is a non-dependent version of `DFunLike.finite`, because dependent instances
    are harder to infer.
 
 You can use these to produce instances for specific `DFunLike` types.