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[bot]]

PR summary fcc7fe288b

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 075fe7eca3ab7f44ea1162d8e184071ffcae929c. There were significant changes against commit cd1f49389b69f1e427def7a7c0ddc46f6a7da7dd:

  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?

[tb65536]

!bench

[leanprover-bot]

Here are the benchmark results for commit fcc7fe288b254fa5f169545fa11e02ed254fe917. There were no significant changes against commit b14fe2c87e1a03a66514f49dc1f50d1c06f5e74d.

[riccardobrasca]

Thanks+

bors merge

[mathlib-bors[bot]]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style