feat(RingTheory/Ideal/Maps): lemmas of ring isomorphisms act on ideals

[mbkybky]

Add some lemmas of ring isomorphisms act on ideals, for example, prove that if e : R ≃+* S is a ring isomorphism, p is an ideal of R, p is prime(resp. maximal), then Ideal.map e p is prime(resp. maximal).

---

[github-actions[bot]]

PR summary cf8534fd94

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ comap_isMaximal_of_equiv + map_isMaximal_of_equiv + mem_map_of_equiv

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.

[mbkybky]

!bench

[leanprover-bot]

Here are the benchmark results for commit cf8534fd94b10dfc10315179593d79dbaf92cfbb. There were no significant changes against commit aea6f296a35d3b88812a1b424543e1da53822850.

[github-actions[bot]]

File	Instructions	%
build	+1.211⬝10⁹	(+0.0%)
Mathlib.RingTheory.Ideal.Maps	+1.430⬝10⁹	(+2.24%)

[mathlib-bors[bot]]

:v: mbkybky can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[mbkybky]

bors r+

[mathlib-bors[bot]]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style