also make use of the newly available notation for the relevant function, where grep can find it

…ing lean4 issue #1910 (#19380)

this PR removes 3 porting notes regarding lean4 issue leanprover/lean4#1910, and makes adaptations to mathlib to make use of the newly working notation. Concretely, that means that `OrderHom.lfp f` now is written `f.lfp`, and similar for `OrderHom.dual` and `OrderHom.gfp`.

there might still be some `dual x` application left inside code with `open OrderHom`, but those are hard to filter for with grep, as there are many declarations named `dual` in different namespaces.

…issue #1910 to refer to lean4 issue #1629 instead (#19381)

These notes refer to the fact that `LinearMap.ker` and friends cannot be used as `f.ker`. However, this fails not because
the function `LinearMap.ker` needs to be coerced to a proper function (which the issue leanprover/lean4#1910 is about), but because the argument `f` has a type (`LinearMap`) that doesn't occur directly as type of an argument to `LinearMap.ker`. The issue leanprover/lean4#1629 *does* suggest a fix for this.

…o refer to lean4 issue #6178 instead  (#19385)

These adaptation notes refer to the `pp_nodot` attribute not doing anything on certain declarations, due to their inability to be used with dot notation. However, now that leanprover/lean4#1910 has been fixed, the limiting factor has become the fact that the pretty printer doesn't work for these kinds of dot notation, which leanprover/lean4#6178 is an issue for.

As such, the links to the blocking lean issue have been changed in this PR.