refactor(RingTheory/Ideal/Pointwise): Make Ideal.IsPrime.smul into an instance

[tb65536]

This PR makes Ideal.IsPrime.smul into an instance (like how Ideal.IsPrime.comap is an instance).

---

[github-actions]

PR summary 075fe7eca3

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

No declarations were harmed in the making of this PR! 🐙

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

[riccardobrasca]

!bench

[leanprover-bot]

Here are the benchmark results for commit 075fe7e.
There were significant changes against commit cd1f493:

  Benchmark      Metric                 Change
  =====================================================
- build          .olean serialization     9.6%
- build          import                  11.1%
- build          initialization           8.4%
- open Mathlib   task-clock              15.8% (16.3 σ)

[riccardobrasca]

Can you please merge master and see if bench gives the same results?