feat(RingTheory/TwoSidedIdeal/Basic): two-sided-ideal as a bimodule

[jjaassoonn]

---

[github-actions[bot]]

PR summary 24700a44cc

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.RingTheory.TwoSidedIdeal.Basic	560	563	+3 (+0.54%)

Import changes for all files

Files	Import difference
Mathlib.RingTheory.TwoSidedIdeal.Basic	3

---

Declarations diff

+ coeAddMonoidHom + coe_mop_smul + coe_smul + instance : SMul R I where smul r x := ⟨r • x.1, I.mul_mem_left _ _ x.2⟩ + instance : SMul Rᵐᵒᵖ I where smul r x := ⟨r • x.1, I.mul_mem_right _ _ x.2⟩ + instance : SMulCommClass R Rᵐᵒᵖ I + leftModule + rightModule + subtype + subtypeMop

You can run this locally as follows

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

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

[kbuzzard]

Thanks!

maintainer merge

[github-actions[bot]]

🚀 Pull request has been placed on the maintainer queue by kbuzzard.

[mattrobball]

!bench

[leanprover-bot]

Here are the benchmark results for commit 24700a44cc5105d4d63f0d4d17910de09d2b78be. There were no significant changes against commit d2e8846f9bb14855a6d84e36552bc60e38bab88f.

[kim-em]

bors merge

[mathlib-bors[bot]]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style