refactor: introduce Ideal.IsTwoSided class for quotients of noncommutative rings

[alreadydone]

---

• depends on: refactor: generalize Mul of Submodule and SMul of Ideal on Submodule to noncommutative setting #17708

[github-actions]

PR summary cb0757f08d

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.RingTheory.Ideal.Colon	945	946	+1 (+0.11%)

Import changes for all files

Files	Import difference
Mathlib.RingTheory.Ideal.Colon	1
Mathlib.LinearAlgebra.TensorProduct.Quotient	68

---

Declarations diff

+ IsTorsionBySet.semilinearMap
+ IsTwoSided
+ LinearEquiv.annihilator_eq
+ LinearMap.annihilator_le_of_injective
+ LinearMap.annihilator_le_of_surjective
+ Module.annihilator
+ Module.mem_annihilator
+ divisionRing
+ exists_right_inv_of_exists_left_inv
+ iSup_mul
+ instance (priority := 100) quotientAlgebra {R} [CommRing R] {I : Ideal A} [I.IsTwoSided]
+ instance : (I ^ n).IsTwoSided
+ instance : (Module.annihilator R M).IsTwoSided := inferInstanceAs (RingHom.ker _).IsTwoSided
+ instance : (ker f).IsTwoSided := inferInstanceAs (Ideal.comap f ⊥).IsTwoSided
+ instance : Coe R (R ⧸ I)
+ instance : I.IsTwoSided := ⟨fun b ha ↦ mul_comm b _ ▸ I.smul_mem _ ha⟩
+ instance : IsCoatomic (Ideal α) := CompleteLattice.coatomic_of_top_compact isCompactElement_top
+ instance : IsTwoSided (⊤ : Ideal α) := ⟨fun _ _ ↦ trivial⟩
+ instance : IsTwoSided (⊥ : Ideal α) := ⟨fun _ h ↦ by rw [h, zero_mul]; exact zero_mem _⟩
+ instance : NonUnitalSemiring (Submodule R A)
+ instance : Pow (Submodule R A) ℕ
+ instance : SMul (AddSubmonoid R) (AddSubmonoid A)
+ instance : SMul (Ideal R) (Submodule R M)
+ instance [I.IsTwoSided] : (I.pi ι).IsTwoSided
+ instance [I.IsTwoSided] : Module (R ⧸ I) (M ⧸ I • (⊤ : Submodule R M))
+ instance [J.IsTwoSided] : (I * J).IsTwoSided
+ instance [K.IsTwoSided] : (comap f K).IsTwoSided
+ instance [NoZeroDivisors R] : NoZeroDivisors (Ideal R)
+ instance {R : Type*} [CommSemiring R] {S : Type*} [Semiring S] [Algebra R S]
+ instance {ι} (I : ι → Ideal α) [∀ i, (I i).IsTwoSided] : (⨅ i, I i).IsTwoSided
+ isTorsionBySet_iff_subset_annihilator
+ isTorsionBySet_of_subset
+ isTorsionBy_iff_mem_annihilator
+ mul_eq_map₂
+ mul_iSup
+ mul_one
+ mul_smul
+ mul_sup
+ npowRec_add
+ npowRec_succ
+ pow_eq_npowRec
+ pow_one
+ pow_succ'
+ pow_zero
+ ring
+ smul_eq_map₂
+ smul_induction_on
+ smul_le_smul
+ smul_mem_smul
+ sup_mul
+ toSpanSingleton_eq_algebra_linearMap
++ pow_add
++ pow_succ
++- smul_le
+-+ mul
- _root_.LinearEquiv.annihilator_eq
- _root_.LinearMap.annihilator_le_of_injective
- _root_.LinearMap.annihilator_le_of_surjective
- _root_.Module.annihilator
- _root_.Module.mem_annihilator
- hasSMul'
- instHasQuotient
- instance (priority := 100) quotientAlgebra {I : Ideal A} [Algebra R A] :
- instance : IsCoatomic (Ideal α) := by
- instance : Module (R ⧸ I) (M ⧸ I • (⊤ : Submodule R M))
- instance : Mul (Ideal R)
- instance : Unique (R ⧸ (⊤ : Ideal R))
- instance {I : Ideal R} : Coe R (R ⧸ I)
- instance {R : Type*} [CommSemiring R] [NoZeroDivisors R] : NoZeroDivisors (Ideal R)
- instance {R : Type*} [CommSemiring R] {S : Type*} [CommRing S] [Algebra R S]

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.

[mathlib4-dependent-issues-bot]

This PR/issue depends on:

• refactor: generalize Mul of Submodule and SMul of Ideal on Submodule to noncommutative setting #17708
  By Dependent Issues (🤖). Happy coding!