doc: fix typo in doc of Functor.mapConst (#13285)

This PR fixes a typo.

---

Additional comment:

I found the description hard to read (in part because the term "constant
function" is not one I encounter frequently enough, and because there is
no explicit constant function in the signature). Would you consider
changing the first sentence from "Mapping a constant function" to
"Replaces the value in a functor with a constant, retaining the
functor's structure" (based on Functor.discard)?

Also, I would write `(fun _ => a)` rather than `Function.const _ a`.

---------

Co-authored-by: Joachim Breitner <mail@joachim-breitner.de>

src/Init/Prelude.lean

@@ -145,7 +145,7 @@ Examples:
 The constant function that ignores its argument.
 
 If `a : α`, then `Function.const β a : β → α` is the “constant function with value `a`”. For all
-arguments `b : β`, `Function.const β a b = a`.
+arguments `b : β`, `Function.const β a b = a`. It is often written directly as `fun _ => a`.
 
 Examples:
  * `Function.const Bool 10 true = 10`
@@ -3754,7 +3754,7 @@ class Functor (f : Type u → Type v) : Type (max (u+1) v) where
   /--
   Mapping a constant function.
 
-  Given `a : α` and `v : f α`, `mapConst a v` is equivalent to `Function.const _ a <$> v`. For some
+  Given `a : α` and `v : f β`, `mapConst a v` is equivalent to `(fun _ => a) <$> v`. For some
   functors, this can be implemented more efficiently; for all other functors, the default
   implementation may be used.
   -/