diff --git a/Mathlib/Algebra/Algebra/Tower.lean b/Mathlib/Algebra/Algebra/Tower.lean
index 895e7aa2ca980..6bee784a5bef6 100644
--- a/Mathlib/Algebra/Algebra/Tower.lean
+++ b/Mathlib/Algebra/Algebra/Tower.lean
@@ -84,14 +84,24 @@ section Module
 
 variable [CommSemiring R] [Semiring A] [Algebra R A]
 
-variable [SMul R M] [MulAction A M] [IsScalarTower R A M]
+variable [MulAction A M]
 
 variable {R} {M}
 
-theorem algebraMap_smul (r : R) (x : M) : algebraMap R A r • x = r • x := by
+theorem algebraMap_smul [SMul R M] [IsScalarTower R A M] (r : R) (x : M) :
+    algebraMap R A r • x = r • x := by
   rw [Algebra.algebraMap_eq_smul_one, smul_assoc, one_smul]
 #align is_scalar_tower.algebra_map_smul IsScalarTower.algebraMap_smul
 
+variable {A} in
+theorem of_algebraMap_smul [SMul R M] (h : ∀ (r : R) (x : M), algebraMap R A r • x = r • x) :
+    IsScalarTower R A M where
+  smul_assoc r a x := by rw [Algebra.smul_def, mul_smul, h]
+
+variable (R M) in
+theorem of_compHom : letI := MulAction.compHom M (algebraMap R A : R →* A); IsScalarTower R A M :=
+  letI := MulAction.compHom M (algebraMap R A : R →* A); of_algebraMap_smul fun _ _ ↦ rfl
+
 end Module
 
 section Semiring
diff --git a/Mathlib/Algebra/Module/Submodule/Map.lean b/Mathlib/Algebra/Module/Submodule/Map.lean
index f8578c6393a88..1739a9bb9fb02 100644
--- a/Mathlib/Algebra/Module/Submodule/Map.lean
+++ b/Mathlib/Algebra/Module/Submodule/Map.lean
@@ -36,8 +36,6 @@ variable [Semiring R] [Semiring R₂] [Semiring R₃]
 variable [AddCommMonoid M] [AddCommMonoid M₂] [AddCommMonoid M₃]
 variable [Module R M] [Module R₂ M₂] [Module R₃ M₃]
 variable {σ₁₂ : R →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R →+* R₃}
-variable {σ₂₁ : R₂ →+* R}
-variable [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂]
 variable [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃]
 variable (p p' : Submodule R M) (q q' : Submodule R₂ M₂)
 variable {x : M}
@@ -142,6 +140,7 @@ end
 
 section SemilinearMap
 
+variable {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂]
 variable {F : Type*} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂]
 
 /-- The pushforward of a submodule by an injective linear map is
@@ -392,16 +391,22 @@ end SemilinearMap
 
 section OrderIso
 
-variable {F : Type*} [EquivLike F M M₂] [SemilinearEquivClass F σ₁₂ M M₂]
+variable [RingHomSurjective σ₁₂] {F : Type*}
 
 /-- A linear isomorphism induces an order isomorphism of submodules. -/
 @[simps symm_apply apply]
-def orderIsoMapComap (f : F) : Submodule R M ≃o Submodule R₂ M₂ where
+def orderIsoMapComapOfBijective [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂]
+    (f : F) (hf : Bijective f) : Submodule R M ≃o Submodule R₂ M₂ where
   toFun := map f
   invFun := comap f
-  left_inv := comap_map_eq_of_injective (EquivLike.injective f)
-  right_inv := map_comap_eq_of_surjective (EquivLike.surjective f)
-  map_rel_iff' := map_le_map_iff_of_injective (EquivLike.injective f) _ _
+  left_inv := comap_map_eq_of_injective hf.injective
+  right_inv := map_comap_eq_of_surjective hf.surjective
+  map_rel_iff' := map_le_map_iff_of_injective hf.injective _ _
+
+/-- A linear isomorphism induces an order isomorphism of submodules. -/
+@[simps! symm_apply apply]
+def orderIsoMapComap [EquivLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] (f : F) :
+    Submodule R M ≃o Submodule R₂ M₂ := orderIsoMapComapOfBijective f (EquivLike.bijective f)
 #align submodule.order_iso_map_comap Submodule.orderIsoMapComap
 
 end OrderIso
diff --git a/Mathlib/Algebra/Module/Torsion.lean b/Mathlib/Algebra/Module/Torsion.lean
index 7e11739e0727a..487c559e72152 100644
--- a/Mathlib/Algebra/Module/Torsion.lean
+++ b/Mathlib/Algebra/Module/Torsion.lean
@@ -232,6 +232,9 @@ def IsTorsion :=
   ∀ ⦃x : M⦄, ∃ a : R⁰, a • x = 0
 #align module.is_torsion Module.IsTorsion
 
+theorem isTorsionBySet_annihilator : IsTorsionBySet R M (Module.annihilator R M) :=
+  fun _ r ↦ Module.mem_annihilator.mp r.2 _
+
 end Module
 
 end Defs
@@ -542,6 +545,11 @@ instance IsTorsionBySet.isScalarTower
     (fun b d x => Quotient.inductionOn' d fun c => (smul_assoc b c x : _))
 #align module.is_torsion_by_set.is_scalar_tower Module.IsTorsionBySet.isScalarTower
 
+/-- Any module is also a modle over the quotient of the ring by the annihilator.
+Not an instance because it causes synthesis failures / timeouts. -/
+def quotientAnnihilator : Module (R ⧸ Module.annihilator R M) M :=
+  (isTorsionBySet_annihilator R M).module
+
 instance : Module (R ⧸ I) (M ⧸ I • (⊤ : Submodule R M)) :=
   IsTorsionBySet.module (R := R) (I := I) fun x r => by
     induction x using Quotient.inductionOn
diff --git a/Mathlib/Algebra/Ring/CompTypeclasses.lean b/Mathlib/Algebra/Ring/CompTypeclasses.lean
index c269c59ccf4e7..c9154c2f0dce8 100644
--- a/Mathlib/Algebra/Ring/CompTypeclasses.lean
+++ b/Mathlib/Algebra/Ring/CompTypeclasses.lean
@@ -198,4 +198,6 @@ theorem comp [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [RingHomSurjective 
       rwa [← RingHom.coe_comp, RingHomCompTriple.comp_eq] at this }
 #align ring_hom_surjective.comp RingHomSurjective.comp
 
+instance (σ : R₁ ≃+* R₂) : RingHomSurjective (σ : R₁ →+* R₂) := ⟨σ.surjective⟩
+
 end RingHomSurjective
diff --git a/Mathlib/Algebra/Ring/Pi.lean b/Mathlib/Algebra/Ring/Pi.lean
index 6fcade548b519..67b427171a5a5 100644
--- a/Mathlib/Algebra/Ring/Pi.lean
+++ b/Mathlib/Algebra/Ring/Pi.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Simon Hudon, Patrick Massot
 -/
 import Mathlib.Algebra.Group.Pi.Lemmas
+import Mathlib.Algebra.Ring.CompTypeclasses
 import Mathlib.Algebra.Ring.Hom.Defs
 
 #align_import algebra.ring.pi from "leanprover-community/mathlib"@"ba2245edf0c8bb155f1569fd9b9492a9b384cde6"
@@ -170,6 +171,10 @@ def Pi.evalRingHom (f : I → Type v) [∀ i, NonAssocSemiring (f i)] (i : I) :
 #align pi.eval_ring_hom Pi.evalRingHom
 #align pi.eval_ring_hom_apply Pi.evalRingHom_apply
 
+instance (f : I → Type*) [∀ i, Semiring (f i)] (i) :
+    RingHomSurjective (Pi.evalRingHom f i) where
+  is_surjective x := ⟨by classical exact (if h : · = i then h ▸ x else 0), by simp⟩
+
 /-- `Function.const` as a `RingHom`. -/
 @[simps]
 def Pi.constRingHom (α β : Type*) [NonAssocSemiring β] : β →+* α → β :=
diff --git a/Mathlib/Algebra/Ring/Prod.lean b/Mathlib/Algebra/Ring/Prod.lean
index ed78852dabf2e..c417ec77726f6 100644
--- a/Mathlib/Algebra/Ring/Prod.lean
+++ b/Mathlib/Algebra/Ring/Prod.lean
@@ -5,6 +5,7 @@ Authors: Johannes Hölzl, Chris Hughes, Mario Carneiro, Yury Kudryashov
 -/
 import Mathlib.Data.Int.Cast.Prod
 import Mathlib.Algebra.Group.Prod
+import Mathlib.Algebra.Ring.CompTypeclasses
 import Mathlib.Algebra.Ring.Equiv
 import Mathlib.Algebra.Order.Group.Prod
 import Mathlib.Algebra.Order.Ring.Defs
@@ -202,6 +203,9 @@ def snd : R × S →+* S :=
   { MonoidHom.snd R S, AddMonoidHom.snd R S with toFun := Prod.snd }
 #align ring_hom.snd RingHom.snd
 
+instance (R S) [Semiring R] [Semiring S] : RingHomSurjective (fst R S) := ⟨(⟨⟨·, 0⟩, rfl⟩)⟩
+instance (R S) [Semiring R] [Semiring S] : RingHomSurjective (snd R S) := ⟨(⟨⟨0, ·⟩, rfl⟩)⟩
+
 variable {R S}
 
 @[simp]
diff --git a/Mathlib/Data/Nat/Interval.lean b/Mathlib/Data/Nat/Interval.lean
index bc84b456d9e3d..49aa5d744c6b8 100644
--- a/Mathlib/Data/Nat/Interval.lean
+++ b/Mathlib/Data/Nat/Interval.lean
@@ -396,4 +396,11 @@ theorem Nat.cauchy_induction_two_mul (seed : ℕ) (hs : P seed.succ)
   Nat.cauchy_induction_mul h 2 seed one_lt_two hs hm n
 #align nat.cauchy_induction_two_mul Nat.cauchy_induction_two_mul
 
+theorem Nat.pow_imp_self_of_one_lt {M} [Monoid M] (k : ℕ) (hk : 1 < k)
+    (P : M → Prop) (hmul : ∀ x y, P x → P (x * y) ∨ P (y * x))
+    (hpow : ∀ x, P (x ^ k) → P x) : ∀ n x, P (x ^ n) → P x :=
+  k.cauchy_induction_mul (fun n ih x hx ↦ ih x <| (hmul _ x hx).elim
+    (fun h ↦ by rwa [_root_.pow_succ']) fun h ↦ by rwa [_root_.pow_succ]) 0 hk
+    (fun x hx ↦ pow_one x ▸ hx) fun n _ hn x hx ↦ hpow x <| hn _ <| (pow_mul x k n).subst hx
+
 end Induction
diff --git a/Mathlib/Data/Polynomial/Eval.lean b/Mathlib/Data/Polynomial/Eval.lean
index 7165050f5f68f..3d0d3ae726a55 100644
--- a/Mathlib/Data/Polynomial/Eval.lean
+++ b/Mathlib/Data/Polynomial/Eval.lean
@@ -837,6 +837,17 @@ theorem map_map [Semiring T] (g : S →+* T) (p : R[X]) : (p.map f).map g = p.ma
 theorem map_id : p.map (RingHom.id _) = p := by simp [Polynomial.ext_iff, coeff_map]
 #align polynomial.map_id Polynomial.map_id
 
+/-- The polynomial ring over a finite product of rings is isomorphic to
+the product of polynomial rings over individual rings. -/
+def piEquiv {ι} [Finite ι] (R : ι → Type*) [∀ i, Semiring (R i)] :
+    (∀ i, R i)[X] ≃+* ∀ i, (R i)[X] :=
+  .ofBijective (Pi.ringHom fun i ↦ mapRingHom (Pi.evalRingHom R i))
+    ⟨fun p q h ↦ by ext n i; simpa using congr_arg (fun p ↦ coeff (p i) n) h,
+      fun p ↦ ⟨.ofFinsupp (.ofSupportFinite (fun n i ↦ coeff (p i) n) <|
+        (Set.finite_iUnion fun i ↦ (p i).support.finite_toSet).subset fun n hn ↦ by
+          simp only [Set.mem_iUnion, Finset.mem_coe, mem_support_iff, Function.mem_support] at hn ⊢
+          contrapose! hn; exact funext hn), by ext i n; exact coeff_map _ _⟩⟩
+
 theorem eval₂_eq_eval_map {x : S} : p.eval₂ f x = (p.map f).eval x := by
   -- Porting note: `apply` → `induction`
   induction p using Polynomial.induction_on' with
diff --git a/Mathlib/Data/Polynomial/Module/Basic.lean b/Mathlib/Data/Polynomial/Module/Basic.lean
index a978368c297b9..1a9fdbb648825 100644
--- a/Mathlib/Data/Polynomial/Module/Basic.lean
+++ b/Mathlib/Data/Polynomial/Module/Basic.lean
@@ -88,6 +88,24 @@ instance instIsScalarTowerOrigPolynomial : IsScalarTower R R[X] <| AEval R M a w
 instance instFinitePolynomial [Finite R M] : Finite R[X] <| AEval R M a :=
   Finite.of_restrictScalars_finite R _ _
 
+/-- Construct an `R[X]`-linear map out of `AEval R M a` from a `R`-linear map out of `M`. -/
+def _root_.LinearMap.ofAEval {N} [AddCommMonoid N] [Module R N] [Module R[X] N]
+    [IsScalarTower R R[X] N] (f : M →ₗ[R] N) (hf : ∀ m : M, f (a • m) = (X : R[X]) • f m) :
+    AEval R M a →ₗ[R[X]] N where
+  __ := f ∘ₗ (of R M a).symm
+  map_smul' p := p.induction_on (fun k m ↦ by simp [C_eq_algebraMap])
+    (fun p q hp hq m ↦ by simp_all [add_smul]) fun n k h m ↦ by
+      simp_rw [RingHom.id_apply, AddHom.toFun_eq_coe, LinearMap.coe_toAddHom,
+        LinearMap.comp_apply, LinearEquiv.coe_toLinearMap] at h ⊢
+      simp_rw [pow_succ', ← mul_assoc, mul_smul _ X, ← hf, ← of_symm_X_smul, ← h]
+
+lemma annihilator_eq_ker_aeval [FaithfulSMul A M] :
+    annihilator R[X] (AEval R M a) = RingHom.ker (aeval a) := by
+  ext p
+  simp_rw [mem_annihilator, RingHom.mem_ker]
+  change (∀ m : M, aeval a p • m = 0) ↔ _
+  exact ⟨fun h ↦ eq_of_smul_eq_smul (α := M) <| by simp [h], fun h ↦ by simp [h]⟩
+
 @[simp]
 lemma annihilator_top_eq_ker_aeval [FaithfulSMul A M] :
     (⊤ : Submodule R[X] <| AEval R M a).annihilator = RingHom.ker (aeval a) := by
diff --git a/Mathlib/FieldTheory/Adjoin.lean b/Mathlib/FieldTheory/Adjoin.lean
index 88922ab7c6e6a..071f3acb085c8 100644
--- a/Mathlib/FieldTheory/Adjoin.lean
+++ b/Mathlib/FieldTheory/Adjoin.lean
@@ -1136,7 +1136,7 @@ noncomputable def adjoin.powerBasis {x : L} (hx : IsIntegral K x) : PowerBasis K
 #align intermediate_field.adjoin.power_basis IntermediateField.adjoin.powerBasis
 
 theorem adjoin.finiteDimensional {x : L} (hx : IsIntegral K x) : FiniteDimensional K K⟮x⟯ :=
-  PowerBasis.finiteDimensional (adjoin.powerBasis hx)
+  (adjoin.powerBasis hx).finite
 #align intermediate_field.adjoin.finite_dimensional IntermediateField.adjoin.finiteDimensional
 
 theorem isAlgebraic_adjoin_simple {x : L} (hx : IsIntegral K x) : Algebra.IsAlgebraic K K⟮x⟯ :=
@@ -1297,7 +1297,7 @@ theorem _root_.Polynomial.irreducible_comp {f g : K[X]} (hfm : f.Monic) (hgm : g
     (this.trans natDegree_comp.symm).ge).irreducible hp₁
   have := Fact.mk hp₁
   let Kx := AdjoinRoot p
-  letI := (AdjoinRoot.powerBasis hp₁.ne_zero).finiteDimensional
+  letI := (AdjoinRoot.powerBasis hp₁.ne_zero).finite
   have key₁ : f = minpoly K (aeval (root p) g) := by
     refine minpoly.eq_of_irreducible_of_monic hf ?_ hfm
     rw [← aeval_comp]
diff --git a/Mathlib/FieldTheory/Minpoly/Field.lean b/Mathlib/FieldTheory/Minpoly/Field.lean
index d8d07d3f53a63..828ad6f87ebea 100644
--- a/Mathlib/FieldTheory/Minpoly/Field.lean
+++ b/Mathlib/FieldTheory/Minpoly/Field.lean
@@ -82,6 +82,9 @@ variable {A x} in
 lemma dvd_iff {p : A[X]} : minpoly A x ∣ p ↔ Polynomial.aeval x p = 0 :=
   ⟨fun ⟨q, hq⟩ ↦ by rw [hq, map_mul, aeval, zero_mul], minpoly.dvd A x⟩
 
+theorem isRadical [IsReduced B] : IsRadical (minpoly A x) := fun n p dvd ↦ by
+  rw [dvd_iff] at dvd ⊢; rw [map_pow] at dvd; exact IsReduced.eq_zero _ ⟨n, dvd⟩
+
 theorem dvd_map_of_isScalarTower (A K : Type*) {R : Type*} [CommRing A] [Field K] [CommRing R]
     [Algebra A K] [Algebra A R] [Algebra K R] [IsScalarTower A K R] (x : R) :
     minpoly K x ∣ (minpoly A x).map (algebraMap A K) := by
diff --git a/Mathlib/LinearAlgebra/AnnihilatingPolynomial.lean b/Mathlib/LinearAlgebra/AnnihilatingPolynomial.lean
index e97b14c002504..9012a5da0c49e 100644
--- a/Mathlib/LinearAlgebra/AnnihilatingPolynomial.lean
+++ b/Mathlib/LinearAlgebra/AnnihilatingPolynomial.lean
@@ -177,6 +177,11 @@ theorem monic_generator_eq_minpoly (a : A) (p : 𝕜[X]) (p_monic : p.Monic)
     · apply monic_annIdealGenerator _ _ ((Associated.ne_zero_iff p_gen).mp h)
 #align polynomial.monic_generator_eq_minpoly Polynomial.monic_generator_eq_minpoly
 
+theorem span_minpoly_eq_annihilator {M} [AddCommGroup M] [Module 𝕜 M] (f : Module.End 𝕜 M) :
+    Ideal.span {minpoly 𝕜 f} = Module.annihilator 𝕜[X] (Module.AEval' f) := by
+  rw [← annIdealGenerator_eq_minpoly, span_singleton_annIdealGenerator]; ext
+  rw [mem_annIdeal_iff_aeval_eq_zero, DFunLike.ext_iff, Module.mem_annihilator]; rfl
+
 end Field
 
 end Polynomial
diff --git a/Mathlib/LinearAlgebra/FreeModule/Norm.lean b/Mathlib/LinearAlgebra/FreeModule/Norm.lean
index 9da4d463fb12e..f54ece69be6dc 100644
--- a/Mathlib/LinearAlgebra/FreeModule/Norm.lean
+++ b/Mathlib/LinearAlgebra/FreeModule/Norm.lean
@@ -65,7 +65,7 @@ instance (b : Basis ι F[X] S) {I : Ideal S} (hI : I ≠ ⊥) (i : ι) :
   -- operations to the `Quotient.lift` level and then end up comparing huge
   -- terms.  We should probably make most of the quotient operations
   -- irreducible so that they don't expose `Quotient.lift` accidentally.
-  refine PowerBasis.finiteDimensional ?_
+  refine PowerBasis.finite ?_
   refine AdjoinRoot.powerBasis ?_
   exact I.smithCoeffs_ne_zero b hI i
 
diff --git a/Mathlib/LinearAlgebra/JordanChevalley.lean b/Mathlib/LinearAlgebra/JordanChevalley.lean
index c506177a6bd4d..8df4486a4a123 100644
--- a/Mathlib/LinearAlgebra/JordanChevalley.lean
+++ b/Mathlib/LinearAlgebra/JordanChevalley.lean
@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Oliver Nash
 -/
 import Mathlib.Dynamics.Newton
-import Mathlib.FieldTheory.Perfect
 import Mathlib.LinearAlgebra.Semisimple
 
 /-!
diff --git a/Mathlib/LinearAlgebra/Projection.lean b/Mathlib/LinearAlgebra/Projection.lean
index 19def9b09d3d2..67c1aea3ce7c4 100644
--- a/Mathlib/LinearAlgebra/Projection.lean
+++ b/Mathlib/LinearAlgebra/Projection.lean
@@ -361,6 +361,21 @@ theorem coe_isComplEquivProj_symm_apply (f : { f : E →ₗ[R] p // ∀ x : p, f
     (p.isComplEquivProj.symm f : Submodule R E) = ker (f : E →ₗ[R] p) := rfl
 #align submodule.coe_is_compl_equiv_proj_symm_apply Submodule.coe_isComplEquivProj_symm_apply
 
+/-- The idempotent endomorphisms of a module with range equal to a submodule are in 1-1
+correspondence with linear maps to the submodule that restrict to the identity on the submodule.-/
+@[simps] def isIdempotentElemEquiv :
+    { f : Module.End R E // IsIdempotentElem f ∧ range f = p } ≃
+    { f : E →ₗ[R] p // ∀ x : p, f x = x } where
+  toFun f := ⟨f.1.codRestrict _ fun x ↦ by simp_rw [← f.2.2]; exact mem_range_self f.1 x,
+    fun ⟨x, hx⟩ ↦ Subtype.ext <| by
+      obtain ⟨x, rfl⟩ := f.2.2.symm ▸ hx
+      exact DFunLike.congr_fun f.2.1 x⟩
+  invFun f := ⟨p.subtype ∘ₗ f.1, LinearMap.ext fun x ↦ by simp [f.2], le_antisymm
+    ((range_comp_le_range _ _).trans_eq p.range_subtype)
+    fun x hx ↦ ⟨x, Subtype.ext_iff.1 <| f.2 ⟨x, hx⟩⟩⟩
+  left_inv _ := rfl
+  right_inv _ := rfl
+
 end Submodule
 
 namespace LinearMap
diff --git a/Mathlib/LinearAlgebra/Semisimple.lean b/Mathlib/LinearAlgebra/Semisimple.lean
index 630bfa0cb64ca..556c4ed0d0dec 100644
--- a/Mathlib/LinearAlgebra/Semisimple.lean
+++ b/Mathlib/LinearAlgebra/Semisimple.lean
@@ -3,12 +3,13 @@ Copyright (c) 2024 Oliver Nash. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Oliver Nash
 -/
-import Mathlib.Algebra.Module.PID
-import Mathlib.Data.Polynomial.Module.FiniteDimensional
-import Mathlib.FieldTheory.Minpoly.Field
+import Mathlib.RingTheory.DedekindDomain.Basic
+import Mathlib.FieldTheory.Perfect
 import Mathlib.LinearAlgebra.Basis.VectorSpace
+import Mathlib.LinearAlgebra.AnnihilatingPolynomial
 import Mathlib.Order.CompleteSublattice
-import Mathlib.RingTheory.Nilpotent
+import Mathlib.RingTheory.Artinian
+import Mathlib.RingTheory.QuotientNilpotent
 import Mathlib.RingTheory.SimpleModule
 
 /-!
@@ -30,13 +31,14 @@ endomorphism. We provide basic definitions and results about such endomorphisms
    that is both nilpotent and semisimple.
  * `Module.End.isSemisimple_of_squarefree_aeval_eq_zero`: an endomorphism that is a root of a
    square-free polynomial is semisimple (in finite dimensions over a field).
-
+ * `Module.End.IsSemisimple.minpoly_squarefree`: the minimal polynomial of a semisimple
+   endomorphism is squarefree.
+ * `IsSemisimple.of_mem_adjoin_pair`: every endomorphism in the subalgebra generated by two
+   commuting semisimple endomorphisms is semisimple, if the base field is perfect.
 ## TODO
 
 In finite dimensions over a field:
- * Sum / difference / product of commuting semisimple endomorphisms is semisimple
  * If semisimple then generalized eigenspace is eigenspace
- * Converse of `Module.End.isSemisimple_of_squarefree_aeval_eq_zero`
  * Restriction of semisimple endomorphism is semisimple
  * Triangularizable iff diagonalisable for semisimple endomorphisms
 
@@ -78,39 +80,16 @@ lemma isSemisimple_id [IsSemisimpleModule R M] : IsSemisimple (LinearMap.id : Mo
 @[simp] lemma isSemisimple_neg : (-f).IsSemisimple ↔ f.IsSemisimple := by simp [isSemisimple_iff]
 
 lemma eq_zero_of_isNilpotent_isSemisimple (hn : IsNilpotent f) (hs : f.IsSemisimple) : f = 0 := by
-  nontriviality M
-  set k := nilpotencyClass f
-  wlog hk : 2 ≤ k
-  · replace hk : k = 0 ∨ k = 1 := by omega
-    rcases hk with (hk₀ : nilpotencyClass f = 0) | (hk₁ : nilpotencyClass f = 1)
-    · rw [← pos_nilpotencyClass_iff, hk₀] at hn; contradiction
-    · exact eq_zero_of_nilpotencyClass_eq_one hk₁
-  let p := LinearMap.ker (f ^ (k - 1))
-  have hp : p ≤ p.comap f := fun x hx ↦ by
-    rw [Submodule.mem_comap, LinearMap.mem_ker, ← LinearMap.mul_apply, ← pow_succ', add_comm,
-      pow_add, pow_one, LinearMap.mul_apply, hx, map_zero]
-  obtain ⟨q, hq₀, hq₁, hq₂⟩ := isSemisimple_iff.mp hs p hp
-  replace hq₂ : q ≠ ⊥ := hq₂.ne_bot_of_ne_top <|
-    fun contra ↦ pow_pred_nilpotencyClass hn <| LinearMap.ker_eq_top.mp contra
-  obtain ⟨m, hm₁ : m ∈ q, hm₀ : m ≠ 0⟩ := q.ne_bot_iff.mp hq₂
-  suffices m ∈ p by
-    exfalso
-    apply hm₀
-    rw [← Submodule.mem_bot (R := R), ← hq₁.eq_bot]
-    exact ⟨this, hm₁⟩
-  replace hm₁ : f m = 0 := by
-    rw [← Submodule.mem_bot (R := R), ← hq₁.eq_bot]
-    refine ⟨(?_ : f m ∈ p), hq₀ hm₁⟩
-    rw [LinearMap.mem_ker, ← LinearMap.mul_apply, ← pow_succ', (by omega : k - 1 + 1 = k),
-      pow_nilpotencyClass hn, LinearMap.zero_apply]
-  rw [LinearMap.mem_ker]
-  exact LinearMap.pow_map_zero_of_le (by omega : 1 ≤ k - 1) hm₁
+  have ⟨n, h0⟩ := hn
+  rw [← aeval_X (R := R) f]; rw [← aeval_X_pow (R := R) f] at h0
+  rw [← RingHom.mem_ker, ← AEval.annihilator_eq_ker_aeval (M := M)] at h0 ⊢
+  exact hs.annihilator_isRadical ⟨n, h0⟩
 
 end CommRing
 
 section field
 
-variable {K : Type*} [Field K] [Module K M] {f : End K M}
+variable {K : Type*} [Field K] [Module K M] {f g : End K M}
 
 lemma IsSemisimple_smul_iff {t : K} (ht : t ≠ 0) :
     (t • f).IsSemisimple ↔ f.IsSemisimple := by
@@ -121,23 +100,99 @@ lemma IsSemisimple_smul (t : K) (h : f.IsSemisimple) :
   wlog ht : t ≠ 0; · simp [not_not.mp ht]
   rwa [IsSemisimple_smul_iff ht]
 
-open UniqueFactorizationMonoid in
-theorem isSemisimple_of_squarefree_aeval_eq_zero [FiniteDimensional K M]
-    {p : K[X]} (hp : Squarefree p) (hpf : aeval f p = 0) : f.IsSemisimple := by
-  classical
-  have := (Submodule.isInternal_prime_power_torsion_of_pid <|
-    AEval.isTorsion_of_finiteDimensional K M f).submodule_iSup_eq_top
-  rw [AEval.annihilator_top_eq_ker_aeval, minpoly.ker_aeval_eq_span_minpoly,
-    Ideal.submodule_span_eq, factors_eq_normalizedFactors] at this
-  refine isSemisimpleModule_of_isSemisimpleModule_submodule'
-    (fun ⟨q, hq₁⟩ ↦ Submodule.isSemisimple_torsionBy_of_irreducible <| Prime.irreducible ?_) this
-  simp only [Multiset.mem_toFinset] at hq₁
-  simp only [prime_pow_iff]
-  refine ⟨Ideal.prime_generator_of_prime (prime_of_normalized_factor q hq₁),
-    Multiset.count_eq_one_of_mem ?_ hq₁⟩
-  have hf : Ideal.span {minpoly K f} ≠ 0 := by simpa using minpoly.ne_zero_of_finite K f
-  rw [← squarefree_iff_nodup_normalizedFactors hf, Ideal.squarefree_span_singleton]
-  exact hp.squarefree_of_dvd (minpoly.dvd K f hpf)
+theorem isSemisimple_of_squarefree_aeval_eq_zero {p : K[X]}
+    (hp : Squarefree p) (hpf : aeval f p = 0) : f.IsSemisimple := by
+  rw [← RingHom.mem_ker, ← AEval.annihilator_eq_ker_aeval (M := M), mem_annihilator,
+      ← IsTorsionBy, ← isTorsionBySet_singleton_iff, isTorsionBySet_iff_is_torsion_by_span] at hpf
+  let R := K[X] ⧸ Ideal.span {p}
+  have : IsReduced R :=
+    (Ideal.isRadical_iff_quotient_reduced _).mp (isRadical_iff_span_singleton.mp hp.isRadical)
+  have : FiniteDimensional K R := (AdjoinRoot.powerBasis hp.ne_zero).finite
+  have : IsArtinianRing R := .of_finite K R
+  have : IsSemisimpleRing R := IsArtinianRing.isSemisimpleRing_of_isReduced R
+  letI : Module R (AEval' f) := Module.IsTorsionBySet.module hpf
+  let e : AEval' f →ₛₗ[Ideal.Quotient.mk (Ideal.span {p})] AEval' f :=
+    { AddMonoidHom.id _ with map_smul' := fun _ _ ↦ rfl }
+  exact (e.isSemisimpleModule_iff_of_bijective bijective_id).mpr inferInstance
+
+variable [FiniteDimensional K M]
+
+section
+
+variable (hf : f.IsSemisimple)
+
+/-- The minimal polynomial of a semisimple endomorphism is square free -/
+theorem IsSemisimple.minpoly_squarefree : Squarefree (minpoly K f) :=
+  IsRadical.squarefree (minpoly.ne_zero <| isIntegral _) <| by
+    rw [isRadical_iff_span_singleton, span_minpoly_eq_annihilator]; exact hf.annihilator_isRadical
+
+protected theorem IsSemisimple.aeval (p : K[X]) : (aeval f p).IsSemisimple :=
+  let R := K[X] ⧸ Ideal.span {minpoly K f}
+  have : Finite K R := (AdjoinRoot.powerBasis' <| minpoly.monic <| isIntegral f).finite
+  have : IsArtinianRing R := .of_finite K R
+  have : IsReduced R := (Ideal.isRadical_iff_quotient_reduced _).mp <|
+    span_minpoly_eq_annihilator K f ▸ hf.annihilator_isRadical
+  isSemisimple_of_squarefree_aeval_eq_zero ((minpoly.isRadical K _).squarefree <|
+    minpoly.ne_zero <| .of_finite K <| Ideal.Quotient.mkₐ K (.span {minpoly K f}) p) <| by
+      rw [← Ideal.Quotient.liftₐ_comp (.span {minpoly K f}) (aeval f)
+        fun a h ↦ by rwa [Ideal.span, ← minpoly.ker_aeval_eq_span_minpoly] at h, aeval_algHom,
+        AlgHom.comp_apply, AlgHom.comp_apply, ← aeval_algHom_apply, minpoly.aeval, map_zero]
+
+theorem IsSemisimple.of_mem_adjoin_singleton {a : End K M}
+    (ha : a ∈ Algebra.adjoin K {f}) : a.IsSemisimple := by
+  rw [Algebra.adjoin_singleton_eq_range_aeval] at ha; obtain ⟨p, rfl⟩ := ha; exact .aeval hf _
+
+protected theorem IsSemisimple.pow (n : ℕ) : (f ^ n).IsSemisimple :=
+  .of_mem_adjoin_singleton hf (pow_mem (Algebra.self_mem_adjoin_singleton _ _) _)
+
+end
+
+section PerfectField
+
+variable [PerfectField K] (comm : Commute f g) (hf : f.IsSemisimple) (hg : g.IsSemisimple)
+
+theorem IsSemisimple.of_mem_adjoin_pair {a : End K M} (ha : a ∈ Algebra.adjoin K {f, g}) :
+    a.IsSemisimple := by
+  let R := K[X] ⧸ Ideal.span {minpoly K f}
+  let S := AdjoinRoot ((minpoly K g).map <| algebraMap K R)
+  have : Finite K R := (AdjoinRoot.powerBasis' <| minpoly.monic <| isIntegral f).finite
+  have : Finite R S := (AdjoinRoot.powerBasis' <| (minpoly.monic <| isIntegral g).map _).finite
+  have : IsScalarTower K R S := .of_algebraMap_eq fun _ ↦ rfl
+  have : Finite K S := .trans R S
+  have : IsArtinianRing R := .of_finite K R
+  have : IsReduced R := (Ideal.isRadical_iff_quotient_reduced _).mp <|
+    span_minpoly_eq_annihilator K f ▸ hf.annihilator_isRadical
+  have : IsReduced S := by
+    simp_rw [AdjoinRoot, ← Ideal.isRadical_iff_quotient_reduced, ← isRadical_iff_span_singleton]
+    exact (PerfectField.separable_iff_squarefree.mpr hg.minpoly_squarefree).map.squarefree.isRadical
+  let φ : S →ₐ[K] End K M := Ideal.Quotient.liftₐ _ (eval₂AlgHom' (Ideal.Quotient.liftₐ _ (aeval f)
+    fun a ↦ ?_) g ?_) ((Ideal.span_singleton_le_iff_mem _).mpr ?_ : _ ≤ RingHom.ker _)
+  rotate_left 1
+  · rw [Ideal.span, ← minpoly.ker_aeval_eq_span_minpoly]; exact id
+  · rintro ⟨p⟩; exact p.induction_on (fun k ↦ by simp [Algebra.commute_algebraMap_left])
+      (fun p q hp hq ↦ by simpa using hp.add_left hq)
+      fun n k ↦ by simpa [pow_succ', ← mul_assoc _ _ X] using (·.mul_left comm)
+  · simpa only [RingHom.mem_ker, eval₂AlgHom'_apply, eval₂_map, AlgHom.comp_algebraMap_of_tower]
+      using minpoly.aeval K g
+  have : Algebra.adjoin K {f, g} ≤ φ.range := Algebra.adjoin_le fun x ↦ by
+    rintro (hx | hx) <;> rw [hx]
+    · exact ⟨AdjoinRoot.of _ (AdjoinRoot.root _), (eval₂_C _ _).trans (aeval_X f)⟩
+    · exact ⟨AdjoinRoot.root _, eval₂_X _ _⟩
+  obtain ⟨p, rfl⟩ := (AlgHom.mem_range _).mp (this ha)
+  refine isSemisimple_of_squarefree_aeval_eq_zero
+    ((minpoly.isRadical K p).squarefree <| minpoly.ne_zero <| .of_finite K p) ?_
+  rw [aeval_algHom, φ.comp_apply, minpoly.aeval, φ.map_zero]
+
+theorem IsSemisimple.add_of_commute : (f + g).IsSemisimple := .of_mem_adjoin_pair
+  comm hf hg <| add_mem (Algebra.subset_adjoin <| .inl rfl) (Algebra.subset_adjoin <| .inr rfl)
+
+theorem IsSemisimple.sub_of_commute : (f - g).IsSemisimple := .of_mem_adjoin_pair
+  comm hf hg <| sub_mem (Algebra.subset_adjoin <| .inl rfl) (Algebra.subset_adjoin <| .inr rfl)
+
+theorem IsSemisimple.mul_of_commute : (f * g).IsSemisimple := .of_mem_adjoin_pair
+  comm hf hg <| mul_mem (Algebra.subset_adjoin <| .inl rfl) (Algebra.subset_adjoin <| .inr rfl)
+
+end PerfectField
 
 end field
 
diff --git a/Mathlib/LinearAlgebra/Span.lean b/Mathlib/LinearAlgebra/Span.lean
index ef4002baa083f..7f56eb1c1f1d4 100644
--- a/Mathlib/LinearAlgebra/Span.lean
+++ b/Mathlib/LinearAlgebra/Span.lean
@@ -5,6 +5,7 @@ Authors: Johannes Hölzl, Mario Carneiro, Kevin Buzzard, Yury Kudryashov, Fréd
   Heather Macbeth
 -/
 import Mathlib.Algebra.Module.Submodule.RestrictScalars
+import Mathlib.Algebra.Ring.Idempotents
 import Mathlib.Data.Set.Pointwise.SMul
 import Mathlib.LinearAlgebra.Basic
 import Mathlib.Order.CompactlyGenerated.Basic
@@ -52,6 +53,20 @@ def span (s : Set M) : Submodule R M :=
   sInf { p | s ⊆ p }
 #align submodule.span Submodule.span
 
+variable {R}
+
+-- Porting note: renamed field to `principal'` and added `principal` to fix explicit argument
+/-- An `R`-submodule of `M` is principal if it is generated by one element. -/
+@[mk_iff]
+class IsPrincipal (S : Submodule R M) : Prop where
+  principal' : ∃ a, S = span R {a}
+#align submodule.is_principal Submodule.IsPrincipal
+
+theorem IsPrincipal.principal (S : Submodule R M) [S.IsPrincipal] :
+    ∃ a, S = span R {a} :=
+  Submodule.IsPrincipal.principal'
+#align submodule.is_principal.principal Submodule.IsPrincipal.principal
+
 end
 
 variable {s t : Set M}
@@ -1019,7 +1034,7 @@ section
 variable (R) (M) [Semiring R] [AddCommMonoid M] [Module R M]
 
 /-- Given an element `x` of a module `M` over `R`, the natural map from
-    `R` to scalar multiples of `x`.-/
+    `R` to scalar multiples of `x`. See also `LinearMap.ringLmapEquivSelf`. -/
 @[simps!]
 def toSpanSingleton (x : M) : R →ₗ[R] M :=
   LinearMap.id.smulRight x
@@ -1043,6 +1058,19 @@ theorem toSpanSingleton_zero : toSpanSingleton R M 0 = 0 := by
   simp
 #align linear_map.to_span_singleton_zero LinearMap.toSpanSingleton_zero
 
+variable {R M}
+
+theorem toSpanSingleton_isIdempotentElem_iff {e : R} :
+    IsIdempotentElem (toSpanSingleton R R e) ↔ IsIdempotentElem e := by
+  simp_rw [IsIdempotentElem, ext_iff, mul_apply, toSpanSingleton_apply, smul_eq_mul, mul_assoc]
+  exact ⟨fun h ↦ by conv_rhs => rw [← one_mul e, ← h, one_mul], fun h _ ↦ by rw [h]⟩
+
+theorem isIdempotentElem_apply_one_iff {f : Module.End R R} :
+    IsIdempotentElem (f 1) ↔ IsIdempotentElem f := by
+  rw [IsIdempotentElem, ← smul_eq_mul, ← map_smul, smul_eq_mul, mul_one, IsIdempotentElem, ext_iff]
+  simp_rw [mul_apply]
+  exact ⟨fun h r ↦ by rw [← mul_one r, ← smul_eq_mul, map_smul, map_smul, h], (· 1)⟩
+
 end
 
 section AddCommMonoid
diff --git a/Mathlib/Order/Atoms.lean b/Mathlib/Order/Atoms.lean
index 84d34fca13f0f..782c600b65ff6 100644
--- a/Mathlib/Order/Atoms.lean
+++ b/Mathlib/Order/Atoms.lean
@@ -731,6 +731,9 @@ protected noncomputable def completeBooleanAlgebra : CompleteBooleanAlgebra α :
         exact le_rfl } -- v4.7.0-rc1 issues
 #align is_simple_order.complete_boolean_algebra IsSimpleOrder.completeBooleanAlgebra
 
+instance : ComplementedLattice α :=
+  letI := IsSimpleOrder.completeBooleanAlgebra (α := α); inferInstance
+
 end IsSimpleOrder
 
 namespace IsSimpleOrder
diff --git a/Mathlib/RepresentationTheory/Maschke.lean b/Mathlib/RepresentationTheory/Maschke.lean
index d0dc49e4c1611..bc7a8475e81b6 100644
--- a/Mathlib/RepresentationTheory/Maschke.lean
+++ b/Mathlib/RepresentationTheory/Maschke.lean
@@ -5,6 +5,7 @@ Authors: Scott Morrison
 -/
 import Mathlib.Algebra.MonoidAlgebra.Basic
 import Mathlib.LinearAlgebra.Basis.VectorSpace
+import Mathlib.RingTheory.SimpleModule
 
 #align_import representation_theory.maschke from "leanprover-community/mathlib"@"70fd9563a21e7b963887c9360bd29b2393e6225a"
 
@@ -144,14 +145,17 @@ namespace MonoidAlgebra
 -- Now we work over a `[Field k]`.
 variable {k : Type u} [Field k] {G : Type u} [Fintype G] [Invertible (Fintype.card G : k)]
 variable [Group G]
-variable {V : Type u} [AddCommGroup V] [Module k V] [Module (MonoidAlgebra k G) V]
-variable [IsScalarTower k (MonoidAlgebra k G) V]
-variable {W : Type u} [AddCommGroup W] [Module k W] [Module (MonoidAlgebra k G) W]
-variable [IsScalarTower k (MonoidAlgebra k G) W]
+variable {V : Type u} [AddCommGroup V] [Module (MonoidAlgebra k G) V]
+variable {W : Type u} [AddCommGroup W] [Module (MonoidAlgebra k G) W]
 
 theorem exists_leftInverse_of_injective (f : V →ₗ[MonoidAlgebra k G] W)
     (hf : LinearMap.ker f = ⊥) :
     ∃ g : W →ₗ[MonoidAlgebra k G] V, g.comp f = LinearMap.id := by
+  let A := MonoidAlgebra k G
+  letI : Module k W := .compHom W (algebraMap k A)
+  letI : Module k V := .compHom V (algebraMap k A)
+  have := IsScalarTower.of_compHom k A W
+  have := IsScalarTower.of_compHom k A V
   obtain ⟨φ, hφ⟩ := (f.restrictScalars k).exists_leftInverse_of_injective <| by
     simp only [hf, Submodule.restrictScalars_bot, LinearMap.ker_restrictScalars]
   refine ⟨φ.equivariantProjection G, DFunLike.ext _ _ ?_⟩
@@ -162,17 +166,21 @@ namespace Submodule
 
 theorem exists_isCompl (p : Submodule (MonoidAlgebra k G) V) :
     ∃ q : Submodule (MonoidAlgebra k G) V, IsCompl p q := by
-  have : IsScalarTower k (MonoidAlgebra k G) p := p.isScalarTower'
   rcases MonoidAlgebra.exists_leftInverse_of_injective p.subtype p.ker_subtype with ⟨f, hf⟩
-  refine ⟨LinearMap.ker f, LinearMap.isCompl_of_proj ?_⟩
-  exact DFunLike.congr_fun hf
+  exact ⟨LinearMap.ker f, LinearMap.isCompl_of_proj <| DFunLike.congr_fun hf⟩
 #align monoid_algebra.submodule.exists_is_compl MonoidAlgebra.Submodule.exists_isCompl
 
-/-- This also implies an instance `IsSemisimpleModule (MonoidAlgebra k G) V`. -/
+/-- This also implies instances `IsSemisimpleModule (MonoidAlgebra k G) V` and
+`IsSemisimpleRing (MonoidAlgebra k G)`. -/
 instance complementedLattice : ComplementedLattice (Submodule (MonoidAlgebra k G) V) :=
   ⟨exists_isCompl⟩
 #align monoid_algebra.submodule.complemented_lattice MonoidAlgebra.Submodule.complementedLattice
 
+instance [AddGroup G] : IsSemisimpleRing (AddMonoidAlgebra k G) :=
+  letI : Invertible (Fintype.card (Multiplicative G) : k) := by
+    rwa [Fintype.card_congr Multiplicative.toAdd]
+  (AddMonoidAlgebra.toMultiplicativeAlgEquiv k G (R := ℕ)).toRingEquiv.symm.isSemisimpleRing
+
 end Submodule
 
 end MonoidAlgebra
diff --git a/Mathlib/RingTheory/Artinian.lean b/Mathlib/RingTheory/Artinian.lean
index 138cca73d86f6..494156d12a3ea 100644
--- a/Mathlib/RingTheory/Artinian.lean
+++ b/Mathlib/RingTheory/Artinian.lean
@@ -3,8 +3,10 @@ Copyright (c) 2021 Chris Hughes. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Hughes
 -/
-import Mathlib.RingTheory.Nakayama
 import Mathlib.Data.SetLike.Fintype
+import Mathlib.Algebra.Divisibility.Prod
+import Mathlib.RingTheory.Nakayama
+import Mathlib.RingTheory.SimpleModule
 import Mathlib.Tactic.RSuffices
 
 #align_import ring_theory.artinian from "leanprover-community/mathlib"@"210657c4ea4a4a7b234392f70a3a2a83346dfa90"
@@ -28,6 +30,21 @@ Let `R` be a ring and let `M` and `P` be `R`-modules. Let `N` be an `R`-submodul
   implemented as the predicate that the `<` relation on submodules is well founded.
 * `IsArtinianRing R` is the proposition that `R` is a left Artinian ring.
 
+## Main results
+
+* `IsArtinianRing.localization_surjective`: the canonical homomorphism from a commutative artinian
+  ring to any localization of itself is surjective.
+
+* `IsArtinianRing.isNilpotent_jacobson_bot`: the Jacobson radical of a commutative artinian ring
+  is a nilpotent ideal. (TODO: generalize to noncommutative rings.)
+
+* `IsArtinianRing.primeSpectrum_finite`, `IsArtinianRing.isMaximal_of_isPrime`: there are only
+  finitely prime ideals in a commutative artinian ring, and each of them is maximal.
+
+* `IsArtinianRing.equivPi`: a reduced commutative artinian ring `R` is isomorphic to a finite
+  product of fields (and therefore is a semisimple ring and a decomposition monoid; moreover
+  `R[X]` is also a decomposition monoid).
+
 ## References
 
 * [M. F. Atiyah and I. G. Macdonald, *Introduction to commutative algebra*][atiyah-macdonald]
@@ -402,6 +419,10 @@ instance isArtinian_of_fg_of_artinian' {R M} [Ring R] [AddCommGroup M] [Module R
   isArtinian_of_linearEquiv (LinearEquiv.ofTop (⊤ : Submodule R M) rfl)
 #align is_artinian_of_fg_of_artinian' isArtinian_of_fg_of_artinian'
 
+theorem IsArtinianRing.of_finite (R S) [CommRing R] [Ring S] [Algebra R S]
+    [IsArtinianRing R] [Module.Finite R S] : IsArtinianRing S :=
+  isArtinian_of_tower R isArtinian_of_fg_of_artinian'
+
 /-- In a module over an artinian ring, the submodule generated by finitely many vectors is
 artinian. -/
 theorem isArtinian_span_of_finite (R) {M} [Ring R] [AddCommGroup M] [Module R M] [IsArtinianRing R]
@@ -513,7 +534,7 @@ lemma primeSpectrum_finite : {I : Ideal R | I.IsPrime}.Finite := by
     inf_le_right.eq_of_not_lt (H (p ⊓ s.inf Subtype.val) ⟨insert p s, by simp⟩)
   rwa [← Subtype.ext <| (@isMaximal_of_isPrime _ _ _ _ q.2).eq_of_le p.2.1 hq2]
 
-variable (R) in
+variable (R)
 /--
 [Stacks Lemma 00J7](https://stacks.math.columbia.edu/tag/00J7)
 -/
@@ -521,5 +542,37 @@ lemma maximal_ideals_finite : {I : Ideal R | I.IsMaximal}.Finite := by
   simp_rw [← isPrime_iff_isMaximal]
   apply primeSpectrum_finite R
 
+@[local instance] lemma subtype_isMaximal_finite : Finite {I : Ideal R | I.IsMaximal} :=
+  (maximal_ideals_finite R).to_subtype
+
+/-- A temporary field instance on the quotients by maximal ideals. -/
+@[local instance] noncomputable def fieldOfSubtypeIsMaximal
+    (I : {I : Ideal R | I.IsMaximal}) : Field (R ⧸ I.1) :=
+  have := mem_setOf.mp I.2; Ideal.Quotient.field I.1
+
+/-- The quotient of a commutative artinian ring by its nilradical is isomorphic to
+a finite product of fields, namely the quotients by the maximal ideals. -/
+noncomputable def quotNilradicalEquivPi :
+    R ⧸ nilradical R ≃+* ∀ I : {I : Ideal R | I.IsMaximal}, R ⧸ I.1 :=
+  .trans (Ideal.quotEquivOfEq <| ext fun x ↦ by simp_rw [mem_nilradical,
+    nilpotent_iff_mem_prime, Submodule.mem_iInf, Subtype.forall, isPrime_iff_isMaximal, mem_setOf])
+  (Ideal.quotientInfRingEquivPiQuotient _ fun I J h ↦
+    Ideal.isCoprime_iff_sup_eq.mpr <| I.2.coprime_of_ne J.2 <| by rwa [Ne, Subtype.coe_inj])
+
+/-- A reduced commutative artinian ring is isomorphic to a finite product of fields,
+namely the quotients by the maximal ideals. -/
+noncomputable def equivPi [IsReduced R] : R ≃+* ∀ I : {I : Ideal R | I.IsMaximal}, R ⧸ I.1 :=
+  .trans (.symm <| .quotientBot R) <| .trans
+    (Ideal.quotEquivOfEq (nilradical_eq_zero R).symm) (quotNilradicalEquivPi R)
+
+instance [IsReduced R] : DecompositionMonoid R := MulEquiv.decompositionMonoid (equivPi R)
+
+instance [IsReduced R] : DecompositionMonoid (Polynomial R) :=
+  MulEquiv.decompositionMonoid <| (Polynomial.mapEquiv <| equivPi R).trans (Polynomial.piEquiv _)
+
+theorem isSemisimpleRing_of_isReduced [IsReduced R] : IsSemisimpleRing R :=
+  (equivPi R).symm.isSemisimpleRing
+
+proof_wanted IsSemisimpleRing.isArtinianRing [IsSemisimpleRing R] : IsArtinianRing R
 
 end IsArtinianRing
diff --git a/Mathlib/RingTheory/Ideal/Basic.lean b/Mathlib/RingTheory/Ideal/Basic.lean
index 2ce4a80eef149..ff999268bb9ae 100644
--- a/Mathlib/RingTheory/Ideal/Basic.lean
+++ b/Mathlib/RingTheory/Ideal/Basic.lean
@@ -41,6 +41,14 @@ def Ideal (R : Type u) [Semiring R] :=
   Submodule R R
 #align ideal Ideal
 
+/-- A ring is a principal ideal ring if all (left) ideals are principal. -/
+@[mk_iff]
+class IsPrincipalIdealRing (R : Type u) [Semiring R] : Prop where
+  principal : ∀ S : Ideal R, S.IsPrincipal
+#align is_principal_ideal_ring IsPrincipalIdealRing
+
+attribute [instance] IsPrincipalIdealRing.principal
+
 section Semiring
 
 namespace Ideal
diff --git a/Mathlib/RingTheory/Ideal/Operations.lean b/Mathlib/RingTheory/Ideal/Operations.lean
index bc05e153db213..bd1bbd892bb3c 100644
--- a/Mathlib/RingTheory/Ideal/Operations.lean
+++ b/Mathlib/RingTheory/Ideal/Operations.lean
@@ -6,6 +6,7 @@ Authors: Kenny Lau
 import Mathlib.Algebra.Algebra.Operations
 import Mathlib.Algebra.Ring.Equiv
 import Mathlib.Data.Nat.Choose.Sum
+import Mathlib.Data.Nat.Interval
 import Mathlib.Data.Fintype.Lattice
 import Mathlib.RingTheory.Coprime.Lemmas
 import Mathlib.RingTheory.Ideal.Basic
@@ -25,11 +26,11 @@ open BigOperators Pointwise
 
 namespace Submodule
 
-variable {R : Type u} {M : Type v} {F : Type*} {G : Type*}
+variable {R : Type u} {M : Type v} {M' F G : Type*}
 
 section CommSemiring
 
-variable [CommSemiring R] [AddCommMonoid M] [Module R M]
+variable [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid M'] [Module R M']
 
 open Pointwise
 
@@ -43,16 +44,39 @@ protected theorem _root_.Ideal.smul_eq_mul (I J : Ideal R) : I • J = I * J :=
   rfl
 #align ideal.smul_eq_mul Ideal.smul_eq_mul
 
+variable (R M) in
+/-- `Module.annihilator R M` is the ideal of all elements `r : R` such that `r • M = 0`. -/
+def _root_.Module.annihilator : Ideal R := LinearMap.ker (LinearMap.lsmul R M)
+
+theorem _root_.Module.mem_annihilator {r} : r ∈ Module.annihilator R M ↔ ∀ m : M, r • m = 0 :=
+  ⟨fun h ↦ (congr($h ·)), (LinearMap.ext ·)⟩
+
+theorem _root_.LinearMap.annihilator_le_of_injective (f : M →ₗ[R] M') (hf : Function.Injective f) :
+    Module.annihilator R M' ≤ Module.annihilator R M := fun x h ↦ by
+  rw [Module.mem_annihilator] at h ⊢; exact fun m ↦ hf (by rw [map_smul, h, f.map_zero])
+
+theorem _root_.LinearMap.annihilator_le_of_surjective (f : M →ₗ[R] M')
+    (hf : Function.Surjective f) : Module.annihilator R M ≤ Module.annihilator R M' := fun x h ↦ by
+  rw [Module.mem_annihilator] at h ⊢
+  intro m; obtain ⟨m, rfl⟩ := hf m
+  rw [← map_smul, h, f.map_zero]
+
+theorem _root_.LinearEquiv.annihilator_eq (e : M ≃ₗ[R] M') :
+    Module.annihilator R M = Module.annihilator R M' :=
+  (e.annihilator_le_of_surjective e.surjective).antisymm (e.annihilator_le_of_injective e.injective)
+
 /-- `N.annihilator` is the ideal of all elements `r : R` such that `r • N = 0`. -/
-def annihilator (N : Submodule R M) : Ideal R :=
-  LinearMap.ker (LinearMap.lsmul R N)
+abbrev annihilator (N : Submodule R M) : Ideal R :=
+  Module.annihilator R N
 #align submodule.annihilator Submodule.annihilator
 
+theorem annihilator_top : (⊤ : Submodule R M).annihilator = Module.annihilator R M :=
+  topEquiv.annihilator_eq
+
 variable {I J : Ideal R} {N P : Submodule R M}
 
-theorem mem_annihilator {r} : r ∈ N.annihilator ↔ ∀ n ∈ N, r • n = (0 : M) :=
-  ⟨fun hr n hn => congr_arg Subtype.val (LinearMap.ext_iff.1 (LinearMap.mem_ker.1 hr) ⟨n, hn⟩),
-    fun h => LinearMap.mem_ker.2 <| LinearMap.ext fun n => Subtype.eq <| h n.1 n.2⟩
+theorem mem_annihilator {r} : r ∈ N.annihilator ↔ ∀ n ∈ N, r • n = (0 : M) := by
+  simp_rw [annihilator, Module.mem_annihilator, Subtype.forall, Subtype.ext_iff]; rfl
 #align submodule.mem_annihilator Submodule.mem_annihilator
 
 theorem mem_annihilator' {r} : r ∈ N.annihilator ↔ N ≤ comap (r • (LinearMap.id : M →ₗ[R] M)) ⊥ :=
@@ -376,6 +400,15 @@ theorem mem_colon' {r} : r ∈ N.colon P ↔ P ≤ comap (r • (LinearMap.id :
   mem_colon
 #align submodule.mem_colon' Submodule.mem_colon'
 
+@[simp]
+theorem colon_top {I : Ideal R} : I.colon ⊤ = I := by
+  simp_rw [SetLike.ext_iff, mem_colon, smul_eq_mul]
+  exact fun x ↦ ⟨fun h ↦ mul_one x ▸ h 1 trivial, fun h _ _ ↦ I.mul_mem_right _ h⟩
+
+@[simp]
+theorem colon_bot : colon ⊥ N = N.annihilator := by
+  simp_rw [SetLike.ext_iff, mem_colon, mem_annihilator, mem_bot, forall_const]
+
 theorem colon_mono (hn : N₁ ≤ N₂) (hp : P₁ ≤ P₂) : N₁.colon P₂ ≤ N₂.colon P₁ := fun _ hrnp =>
   mem_colon.2 fun p₁ hp₁ => hn <| mem_colon.1 hrnp p₁ <| hp hp₁
 #align submodule.colon_mono Submodule.colon_mono
@@ -409,6 +442,14 @@ theorem _root_.Ideal.mem_colon_singleton {I : Ideal R} {x r : R} :
   simp only [← Ideal.submodule_span_eq, Submodule.mem_colon_singleton, smul_eq_mul]
 #align ideal.mem_colon_singleton Ideal.mem_colon_singleton
 
+theorem annihilator_quotient {N : Submodule R M} :
+    Module.annihilator R (M ⧸ N) = N.colon ⊤ := by
+  simp_rw [SetLike.ext_iff, Module.mem_annihilator, colon, mem_annihilator, map_top,
+    LinearMap.range_eq_top.mpr (mkQ_surjective N), mem_top, forall_true_left, forall_const]
+
+theorem _root_.Ideal.annihilator_quotient {I : Ideal R} : Module.annihilator R (R ⧸ I) = I := by
+  rw [Submodule.annihilator_quotient, colon_top]
+
 end CommRing
 
 end Submodule
@@ -940,6 +981,8 @@ def radical (I : Ideal R) : Ideal R where
   smul_mem' {r s} := by exact fun ⟨n, h⟩ ↦ ⟨n, (mul_pow r s n).symm ▸ I.mul_mem_left (r ^ n) h⟩
 #align ideal.radical Ideal.radical
 
+theorem mem_radical_iff {r : R} : r ∈ I.radical ↔ ∃ n : ℕ, r ^ n ∈ I := Iff.rfl
+
 /-- An ideal is radical if it contains its radical. -/
 def IsRadical (I : Ideal R) : Prop :=
   I.radical ≤ I
@@ -956,6 +999,10 @@ theorem radical_eq_iff : I.radical = I ↔ I.IsRadical := by
 alias ⟨_, IsRadical.radical⟩ := radical_eq_iff
 #align ideal.is_radical.radical Ideal.IsRadical.radical
 
+theorem isRadical_iff_pow_one_lt (k : ℕ) (hk : 1 < k) : I.IsRadical ↔ ∀ r, r ^ k ∈ I → r ∈ I :=
+  ⟨fun h _r hr ↦ h ⟨k, hr⟩, fun h x ⟨n, hx⟩ ↦
+    k.pow_imp_self_of_one_lt hk _ (fun _ _ ↦ .inr ∘ I.smul_mem _) h n x hx⟩
+
 variable (R)
 
 theorem radical_top : (radical ⊤ : Ideal R) = ⊤ :=
@@ -1018,6 +1065,17 @@ theorem radical_inf : radical (I ⊓ J) = radical I ⊓ radical J :=
       (pow_add r m n).symm ▸ J.mul_mem_left _ hrn⟩
 #align ideal.radical_inf Ideal.radical_inf
 
+variable {I J} in
+theorem IsRadical.inf (hI : IsRadical I) (hJ : IsRadical J) : IsRadical (I ⊓ J) := by
+  rw [IsRadical, radical_inf]; exact inf_le_inf hI hJ
+
+/-- The reverse inclusion does not hold for e.g. `I := fun n : ℕ ↦ Ideal.span {(2 ^ n : ℤ)}`. -/
+theorem radical_iInf_le {ι} (I : ι → Ideal R) : radical (⨅ i, I i) ≤ ⨅ i, radical (I i) :=
+  le_iInf fun _ ↦ radical_mono (iInf_le _ _)
+
+theorem isRadical_iInf {ι} (I : ι → Ideal R) (hI : ∀ i, IsRadical (I i)) : IsRadical (⨅ i, I i) :=
+  (radical_iInf_le I).trans (iInf_mono hI)
+
 theorem radical_mul : radical (I * J) = radical I ⊓ radical J := by
   refine le_antisymm ?_ fun r ⟨⟨m, hrm⟩, ⟨n, hrn⟩⟩ =>
     ⟨m + n, (pow_add r m n).symm ▸ mul_mem_mul hrm hrn⟩
diff --git a/Mathlib/RingTheory/Ideal/QuotientOperations.lean b/Mathlib/RingTheory/Ideal/QuotientOperations.lean
index b9fac1005ad63..e3adc081a69dc 100644
--- a/Mathlib/RingTheory/Ideal/QuotientOperations.lean
+++ b/Mathlib/RingTheory/Ideal/QuotientOperations.lean
@@ -91,6 +91,12 @@ theorem quotientKerEquivOfRightInverse.Symm.apply {g : S → R} (hf : Function.R
   rfl
 #align ring_hom.quotient_ker_equiv_of_right_inverse.symm.apply RingHom.quotientKerEquivOfRightInverse.Symm.apply
 
+variable (R) in
+/-- The quotient of a ring by he zero ideal is isomorphic to the ring itself. -/
+def _root_.RingEquiv.quotientBot : R ⧸ (⊥ : Ideal R) ≃+* R :=
+  (Ideal.quotEquivOfEq (RingHom.ker_coe_equiv <| .refl _).symm).trans <|
+    quotientKerEquivOfRightInverse (f := .id R) (g := _root_.id) fun _ ↦ rfl
+
 /-- The **first isomorphism theorem** for commutative rings, surjective case. -/
 noncomputable def quotientKerEquivOfSurjective (hf : Function.Surjective f) : R ⧸ (ker f) ≃+* S :=
   quotientKerEquivOfRightInverse (Classical.choose_spec hf.hasRightInverse)
diff --git a/Mathlib/RingTheory/Localization/Submodule.lean b/Mathlib/RingTheory/Localization/Submodule.lean
index 2d9198cb24510..bbcf88c9d7515 100644
--- a/Mathlib/RingTheory/Localization/Submodule.lean
+++ b/Mathlib/RingTheory/Localization/Submodule.lean
@@ -5,7 +5,7 @@ Authors: Kenny Lau, Mario Carneiro, Johan Commelin, Amelia Livingston, Anne Baan
 -/
 import Mathlib.RingTheory.Localization.FractionRing
 import Mathlib.RingTheory.Localization.Ideal
-import Mathlib.RingTheory.PrincipalIdealDomain
+import Mathlib.RingTheory.Noetherian
 
 #align_import ring_theory.localization.submodule from "leanprover-community/mathlib"@"1ebb20602a8caef435ce47f6373e1aa40851a177"
 
diff --git a/Mathlib/RingTheory/Nilpotent.lean b/Mathlib/RingTheory/Nilpotent.lean
index 8f9ec22874b83..b48f95ec3df47 100644
--- a/Mathlib/RingTheory/Nilpotent.lean
+++ b/Mathlib/RingTheory/Nilpotent.lean
@@ -291,9 +291,7 @@ theorem isRadical_iff_span_singleton [CommSemiring R] :
 
 theorem isRadical_iff_pow_one_lt [MonoidWithZero R] (k : ℕ) (hk : 1 < k) :
     IsRadical y ↔ ∀ x, y ∣ x ^ k → y ∣ x :=
-  ⟨fun h x => h k x, fun h =>
-    k.cauchy_induction_mul (fun n h x hd => h x <| (pow_succ' x n).symm ▸ hd.mul_right x) 0 hk
-      (fun x hd => pow_one x ▸ hd) fun n _ hn x hd => h x <| hn _ <| (pow_mul x k n).subst hd⟩
+  ⟨(· k), k.pow_imp_self_of_one_lt hk _ fun _ _ h ↦ .inl (dvd_mul_of_dvd_left h _)⟩
 #align is_radical_iff_pow_one_lt isRadical_iff_pow_one_lt
 
 theorem isReduced_iff_pow_one_lt [MonoidWithZero R] (k : ℕ) (hk : 1 < k) :
diff --git a/Mathlib/RingTheory/Polynomial/Eisenstein/IsIntegral.lean b/Mathlib/RingTheory/Polynomial/Eisenstein/IsIntegral.lean
index 2f8c1afef84bb..16f92c9824f41 100644
--- a/Mathlib/RingTheory/Polynomial/Eisenstein/IsIntegral.lean
+++ b/Mathlib/RingTheory/Polynomial/Eisenstein/IsIntegral.lean
@@ -140,7 +140,7 @@ theorem dvd_coeff_zero_of_aeval_eq_prime_smul_of_minpoly_isEisensteinAt {B : Pow
     (hp : Prime p) (hBint : IsIntegral R B.gen) {z : L} {Q : R[X]} (hQ : aeval B.gen Q = p • z)
     (hzint : IsIntegral R z) (hei : (minpoly R B.gen).IsEisensteinAt 𝓟) : p ∣ Q.coeff 0 := by
   -- First define some abbreviations.
-  letI := B.finiteDimensional
+  letI := B.finite
   let P := minpoly R B.gen
   obtain ⟨n, hn⟩ := Nat.exists_eq_succ_of_ne_zero B.dim_pos.ne'
   have finrank_K_L : FiniteDimensional.finrank K L = B.dim := B.finrank
@@ -243,7 +243,7 @@ theorem mem_adjoin_of_smul_prime_smul_of_minpoly_isEisensteinAt {B : PowerBasis
   -- First define some abbreviations.
   have hndiv : ¬p ^ 2 ∣ (minpoly R B.gen).coeff 0 := fun h =>
     hei.not_mem ((span_singleton_pow p 2).symm ▸ Ideal.mem_span_singleton.2 h)
-  letI := finiteDimensional B
+  have := B.finite
   set P := minpoly R B.gen with hP
   obtain ⟨n, hn⟩ := Nat.exists_eq_succ_of_ne_zero B.dim_pos.ne'
   haveI : NoZeroSMulDivisors R L := NoZeroSMulDivisors.trans R K L
diff --git a/Mathlib/RingTheory/PowerBasis.lean b/Mathlib/RingTheory/PowerBasis.lean
index 8bff3601c53fa..a9840cf9dbda9 100644
--- a/Mathlib/RingTheory/PowerBasis.lean
+++ b/Mathlib/RingTheory/PowerBasis.lean
@@ -78,9 +78,9 @@ theorem coe_basis (pb : PowerBasis R S) : ⇑pb.basis = fun i : Fin pb.dim => pb
 #align power_basis.coe_basis PowerBasis.coe_basis
 
 /-- Cannot be an instance because `PowerBasis` cannot be a class. -/
-theorem finiteDimensional [Algebra K S] (pb : PowerBasis K S) : FiniteDimensional K S :=
-  FiniteDimensional.of_fintype_basis pb.basis
-#align power_basis.finite_dimensional PowerBasis.finiteDimensional
+theorem finite (pb : PowerBasis R S) : Module.Finite R S := .of_basis pb.basis
+#align power_basis.finite_dimensional PowerBasis.finite
+@[deprecated] alias finiteDimensional := PowerBasis.finite
 
 theorem finrank [StrongRankCondition R] (pb : PowerBasis R S) :
     FiniteDimensional.finrank R S = pb.dim := by
diff --git a/Mathlib/RingTheory/PrincipalIdealDomain.lean b/Mathlib/RingTheory/PrincipalIdealDomain.lean
index f8b75da2e6584..f354391068da1 100644
--- a/Mathlib/RingTheory/PrincipalIdealDomain.lean
+++ b/Mathlib/RingTheory/PrincipalIdealDomain.lean
@@ -29,7 +29,7 @@ Theorems about PID's are in the `principal_ideal_ring` namespace.
 
 - `to_maximal_ideal`: a non-zero prime ideal in a PID is maximal.
 - `EuclideanDomain.to_principal_ideal_domain` : a Euclidean domain is a PID.
-- `IsBezout.toGCDDomain`: Every Bézout domain is a GCD domain. This is not an instance.
+- `IsBezout.nonemptyGCDMonoid`: Every Bézout domain is a GCD domain.
 
 -/
 
@@ -46,18 +46,6 @@ section
 
 variable [Ring R] [AddCommGroup M] [Module R M]
 
--- Porting note: renamed field to `principal'` and added `principal` to fix explicit argument
-/-- An `R`-submodule of `M` is principal if it is generated by one element. -/
-@[mk_iff]
-class Submodule.IsPrincipal (S : Submodule R M) : Prop where
-  principal' : ∃ a, S = span R {a}
-#align submodule.is_principal Submodule.IsPrincipal
-
-theorem Submodule.IsPrincipal.principal (S : Submodule R M) [S.IsPrincipal] :
-    ∃ a, S = span R {a} :=
-  Submodule.IsPrincipal.principal'
-#align submodule.is_principal.principal Submodule.IsPrincipal.principal
-
 instance bot_isPrincipal : (⊥ : Submodule R M).IsPrincipal :=
   ⟨⟨0, by simp⟩⟩
 #align bot_is_principal bot_isPrincipal
@@ -68,14 +56,6 @@ instance top_isPrincipal : (⊤ : Submodule R R).IsPrincipal :=
 
 variable (R)
 
-/-- A ring is a principal ideal ring if all (left) ideals are principal. -/
-@[mk_iff]
-class IsPrincipalIdealRing (R : Type u) [Ring R] : Prop where
-  principal : ∀ S : Ideal R, S.IsPrincipal
-#align is_principal_ideal_ring IsPrincipalIdealRing
-
-attribute [instance] IsPrincipalIdealRing.principal
-
 /-- A Bézout ring is a ring whose finitely generated ideals are principal. -/
 class IsBezout : Prop where
   /-- Any finitely generated ideal is principal. -/
@@ -238,7 +218,8 @@ noncomputable def toGCDDomain [IsBezout R] [IsDomain R] [DecidableEq R] : GCDMon
   gcdMonoidOfGCD (gcd · ·) (gcd_dvd_left · ·) (gcd_dvd_right · ·) dvd_gcd
 #align is_bezout.to_gcd_domain IsBezout.toGCDDomain
 
-instance [IsBezout R] [IsDomain R] : Nonempty (GCDMonoid R) := by classical exact ⟨toGCDDomain R⟩
+instance nonemptyGCDMonoid [IsBezout R] [IsDomain R] : Nonempty (GCDMonoid R) := by
+  classical exact ⟨toGCDDomain R⟩
 
 end IsBezout
 
diff --git a/Mathlib/RingTheory/SimpleModule.lean b/Mathlib/RingTheory/SimpleModule.lean
index a3c2e585bcac8..9c319c3f565eb 100644
--- a/Mathlib/RingTheory/SimpleModule.lean
+++ b/Mathlib/RingTheory/SimpleModule.lean
@@ -4,8 +4,10 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Aaron Anderson
 -/
 import Mathlib.LinearAlgebra.Isomorphisms
+import Mathlib.LinearAlgebra.Projection
 import Mathlib.Order.JordanHolder
 import Mathlib.Order.CompactlyGenerated.Intervals
+import Mathlib.LinearAlgebra.FiniteDimensional
 
 #align_import ring_theory.simple_module from "leanprover-community/mathlib"@"cce7f68a7eaadadf74c82bbac20721cdc03a1cc1"
 
@@ -21,7 +23,20 @@ import Mathlib.Order.CompactlyGenerated.Intervals
 
 ## Main Results
   * Schur's Lemma: `bijective_or_eq_zero` shows that a linear map between simple modules
-  is either bijective or 0, leading to a `DivisionRing` structure on the endomorphism ring.
+    is either bijective or 0, leading to a `DivisionRing` structure on the endomorphism ring.
+  * `isSimpleModule_iff_quot_maximal`:
+    a module is simple iff it's isomorphic to the quotient of the ring by a maximal left ideal.
+  * `sSup_simples_eq_top_iff_isSemisimpleModule`:
+    a module is semisimple iff it is generated by its simple submodules.
+  * `IsSemisimpleModule.annihilator_isRadical`:
+    the annihilator of a semisimple module over a commutative ring is a radical ideal.
+  * `IsSemisimpleModule.submodule`, `IsSemisimpleModule.quotient`:
+    any submodule or quotient module of a semisimple module is semisimple.
+  * `isSemisimpleModule_of_isSemisimpleModule_submodule`:
+    a module generated by semisimple submodules is itself semisimple.
+  * `IsSemisimpleRing.isSemisimpleModule`: every module over a semisimple ring is semisimple.
+  * `instIsSemisimpleRingForAllRing`: a finite product of semisimple rings is semisimple.
+  * `RingHom.isSemisimpleRing_of_surjective`: any quotient of a semisimple ring is semisimple.
 
 ## TODO
   * Artin-Wedderburn Theory
@@ -30,7 +45,7 @@ import Mathlib.Order.CompactlyGenerated.Intervals
 -/
 
 
-variable {ι : Type*} (R : Type*) [Ring R] (M : Type*) [AddCommGroup M] [Module R M]
+variable {ι : Type*} (R S : Type*) [Ring R] [Ring S] (M : Type*) [AddCommGroup M] [Module R M]
 
 /-- A module is simple when it has only two submodules, `⊥` and `⊤`. -/
 abbrev IsSimpleModule :=
@@ -43,6 +58,12 @@ abbrev IsSemisimpleModule :=
   ComplementedLattice (Submodule R M)
 #align is_semisimple_module IsSemisimpleModule
 
+/-- A ring is semisimple if it is semisimple as a module over itself. -/
+abbrev IsSemisimpleRing := IsSemisimpleModule R R
+
+theorem RingEquiv.isSemisimpleRing (e : R ≃+* S) [IsSemisimpleRing R] : IsSemisimpleRing S :=
+  (Submodule.orderIsoMapComap e.toSemilinearEquiv).complementedLattice
+
 -- Making this an instance causes the linter to complain of "dangerous instances"
 theorem IsSimpleModule.nontrivial [IsSimpleModule R M] : Nontrivial M :=
   ⟨⟨0, by
@@ -52,8 +73,11 @@ theorem IsSimpleModule.nontrivial [IsSimpleModule R M] : Nontrivial M :=
       simp [Submodule.mem_bot, Submodule.mem_top, h x]⟩⟩
 #align is_simple_module.nontrivial IsSimpleModule.nontrivial
 
-variable {R} {M} -- Porting note: had break line or all hell breaks loose
-variable {m : Submodule R M} {N : Type*} [AddCommGroup N] [Module R N]
+variable {m : Submodule R M} {N : Type*} [AddCommGroup N] [Module R N] {R S M}
+
+theorem LinearMap.isSimpleModule_iff_of_bijective [Module S N] {σ : R →+* S} [RingHomSurjective σ]
+    (l : M →ₛₗ[σ] N) (hl : Function.Bijective l) : IsSimpleModule R M ↔ IsSimpleModule S N :=
+  (Submodule.orderIsoMapComapOfBijective l hl).isSimpleOrder_iff
 
 theorem IsSimpleModule.congr (l : M ≃ₗ[R] N) [IsSimpleModule R N] : IsSimpleModule R M :=
   (Submodule.orderIsoMapComap l).isSimpleOrder
@@ -90,12 +114,80 @@ theorem isAtom : IsAtom m :=
   isSimpleModule_iff_isAtom.1 hm
 #align is_simple_module.is_atom IsSimpleModule.isAtom
 
+variable [IsSimpleModule R M] (R)
+open LinearMap
+
+theorem span_singleton_eq_top {m : M} (hm : m ≠ 0) : Submodule.span R {m} = ⊤ :=
+  (eq_bot_or_eq_top _).resolve_left fun h ↦ hm (h.le <| Submodule.mem_span_singleton_self m)
+
+instance (S : Submodule R M) : S.IsPrincipal where
+  principal' := by
+    obtain rfl | rfl := eq_bot_or_eq_top S
+    · exact ⟨0, Submodule.span_zero.symm⟩
+    have := IsSimpleModule.nontrivial R M
+    have ⟨m, hm⟩ := exists_ne (0 : M)
+    exact ⟨m, (span_singleton_eq_top R hm).symm⟩
+
+theorem toSpanSingleton_surjective {m : M} (hm : m ≠ 0) :
+    Function.Surjective (toSpanSingleton R M m) := by
+  rw [← range_eq_top, ← span_singleton_eq_range, span_singleton_eq_top R hm]
+
+theorem ker_toSpanSingleton_isMaximal {m : M} (hm : m ≠ 0) :
+    Ideal.IsMaximal (ker (toSpanSingleton R M m)) := by
+  rw [Ideal.isMaximal_def, ← isSimpleModule_iff_isCoatom]
+  exact congr (quotKerEquivOfSurjective _ <| toSpanSingleton_surjective R hm)
+
 end IsSimpleModule
 
-theorem is_semisimple_of_sSup_simples_eq_top
+open IsSimpleModule in
+/-- A module is simple iff it's isomorphic to the quotient of the ring by a maximal left ideal
+(not necessarily unique if the ring is not commutative). -/
+theorem isSimpleModule_iff_quot_maximal :
+    IsSimpleModule R M ↔ ∃ I : Ideal R, I.IsMaximal ∧ Nonempty (M ≃ₗ[R] R ⧸ I) := by
+  refine ⟨fun h ↦ ?_, fun ⟨I, ⟨coatom⟩, ⟨equiv⟩⟩ ↦ ?_⟩
+  · have := IsSimpleModule.nontrivial R M
+    have ⟨m, hm⟩ := exists_ne (0 : M)
+    exact ⟨_, ker_toSpanSingleton_isMaximal R hm,
+      ⟨(LinearMap.quotKerEquivOfSurjective _ <| toSpanSingleton_surjective R hm).symm⟩⟩
+  · convert congr equiv; rwa [isSimpleModule_iff_isCoatom]
+
+/-- In general, the annihilator of a simple module is called a primitive ideal, and it is
+always a two-sided prime ideal, but mathlib's `Ideal.IsPrime` is not the correct definition
+for noncommutative rings. -/
+theorem IsSimpleModule.annihilator_isMaximal {R} [CommRing R] [Module R M]
+    [simple : IsSimpleModule R M] : (Module.annihilator R M).IsMaximal := by
+  have ⟨I, max, ⟨e⟩⟩ := isSimpleModule_iff_quot_maximal.mp simple
+  rwa [e.annihilator_eq, I.annihilator_quotient]
+
+theorem isSimpleModule_iff_toSpanSingleton_surjective : IsSimpleModule R M ↔
+    Nontrivial M ∧ ∀ x : M, x ≠ 0 → Function.Surjective (LinearMap.toSpanSingleton R M x) :=
+  ⟨fun h ↦ ⟨h.nontrivial, fun _ ↦ h.toSpanSingleton_surjective⟩, fun ⟨_, h⟩ ↦
+    ⟨fun m ↦ or_iff_not_imp_left.mpr fun ne_bot ↦
+      have ⟨x, hxm, hx0⟩ := m.ne_bot_iff.mp ne_bot
+      top_unique <| fun z _ ↦ by obtain ⟨y, rfl⟩ := h x hx0 z; exact m.smul_mem _ hxm⟩⟩
+
+/-- A ring is a simple module over itself iff it is a division ring. -/
+theorem isSimpleModule_self_iff_isUnit :
+    IsSimpleModule R R ↔ Nontrivial R ∧ ∀ x : R, x ≠ 0 → IsUnit x :=
+  isSimpleModule_iff_toSpanSingleton_surjective.trans <| and_congr_right fun _ ↦ by
+    refine ⟨fun h x hx ↦ ?_, fun h x hx ↦ (h x hx).unit.mulRight_bijective.surjective⟩
+    obtain ⟨y, hyx : y * x = 1⟩ := h x hx 1
+    have hy : y ≠ 0 := left_ne_zero_of_mul (hyx.symm ▸ one_ne_zero)
+    obtain ⟨z, hzy : z * y = 1⟩ := h y hy 1
+    exact ⟨⟨x, y, left_inv_eq_right_inv hzy hyx ▸ hzy, hyx⟩, rfl⟩
+
+theorem isSimpleModule_iff_finrank_eq_one {R} [DivisionRing R] [Module R M] :
+    IsSimpleModule R M ↔ FiniteDimensional.finrank R M = 1 :=
+  ⟨fun h ↦ have := h.nontrivial; have ⟨v, hv⟩ := exists_ne (0 : M)
+    (finrank_eq_one_iff_of_nonzero' v hv).mpr (IsSimpleModule.toSpanSingleton_surjective R hv),
+  is_simple_module_of_finrank_eq_one⟩
+
+theorem IsSemisimpleModule.of_sSup_simples_eq_top
     (h : sSup { m : Submodule R M | IsSimpleModule R m } = ⊤) : IsSemisimpleModule R M :=
   complementedLattice_of_sSup_atoms_eq_top (by simp_rw [← h, isSimpleModule_iff_isAtom])
-#align is_semisimple_of_Sup_simples_eq_top is_semisimple_of_sSup_simples_eq_top
+#align is_semisimple_of_Sup_simples_eq_top IsSemisimpleModule.of_sSup_simples_eq_top
+@[deprecated]
+alias is_semisimple_of_sSup_simples_eq_top := IsSemisimpleModule.of_sSup_simples_eq_top
 
 namespace IsSemisimpleModule
 
@@ -106,20 +198,59 @@ theorem sSup_simples_eq_top : sSup { m : Submodule R M | IsSimpleModule R m } =
   exact sSup_atoms_eq_top
 #align is_semisimple_module.Sup_simples_eq_top IsSemisimpleModule.sSup_simples_eq_top
 
-instance is_semisimple_submodule {m : Submodule R M} : IsSemisimpleModule R m :=
+/-- The annihilator of a semisimple module over a commutative ring is a radical ideal. -/
+theorem annihilator_isRadical {R} [CommRing R] [Module R M] [IsSemisimpleModule R M] :
+    (Module.annihilator R M).IsRadical := by
+  rw [← Submodule.annihilator_top, ← sSup_simples_eq_top, sSup_eq_iSup', Submodule.annihilator_iSup]
+  exact Ideal.isRadical_iInf _ fun i ↦ (i.2.annihilator_isMaximal).isPrime.isRadical
+
+instance submodule {m : Submodule R M} : IsSemisimpleModule R m :=
   haveI f : Submodule R m ≃o Set.Iic m := Submodule.MapSubtype.relIso m
   f.complementedLattice_iff.2 IsModularLattice.complementedLattice_Iic
-#align is_semisimple_module.is_semisimple_submodule IsSemisimpleModule.is_semisimple_submodule
+#align is_semisimple_module.is_semisimple_submodule IsSemisimpleModule.submodule
+
+open LinearMap
+
+theorem congr [IsSemisimpleModule R N] (e : M ≃ₗ[R] N) : IsSemisimpleModule R M :=
+  (Submodule.orderIsoMapComap e.symm).complementedLattice
+
+instance quotient : IsSemisimpleModule R (M ⧸ m) :=
+  have ⟨P, compl⟩ := exists_isCompl m
+  .congr (m.quotientEquivOfIsCompl P compl)
+
+-- does not work as an instance, not sure why
+protected theorem range [IsSemisimpleModule R M] (f : M →ₗ[R] N) : IsSemisimpleModule R (range f) :=
+  .congr (quotKerEquivRange _).symm
+
+section
+
+variable [Module S N] {σ : R →+* S} [RingHomSurjective σ] (l : M →ₛₗ[σ] N)
+
+theorem _root_.LinearMap.isSemisimpleModule_iff_of_bijective (hl : Function.Bijective l) :
+    IsSemisimpleModule R M ↔ IsSemisimpleModule S N :=
+  (Submodule.orderIsoMapComapOfBijective l hl).complementedLattice_iff
+
+-- TODO: generalize Submodule.equivMapOfInjective from InvPair to RingHomSurjective
+proof_wanted _root_.LinearMap.isSemisimpleModule_of_injective (_ : Function.Injective l)
+    [IsSemisimpleModule S N] : IsSemisimpleModule R M
+
+--TODO: generalize LinearMap.quotKerEquivOfSurjective to SemilinearMaps + RingHomSurjective
+proof_wanted _root_.LinearMap.isSemisimpleModule_of_surjective (_ : Function.Surjective l)
+    [IsSemisimpleModule R M] : IsSemisimpleModule S N
+
+end
 
 end IsSemisimpleModule
 
-theorem is_semisimple_iff_top_eq_sSup_simples :
+/-- A module is semisimple iff it is generated by its simple submodules. -/
+theorem sSup_simples_eq_top_iff_isSemisimpleModule :
     sSup { m : Submodule R M | IsSimpleModule R m } = ⊤ ↔ IsSemisimpleModule R M :=
-  ⟨is_semisimple_of_sSup_simples_eq_top, by
-    intro
-    exact IsSemisimpleModule.sSup_simples_eq_top⟩
-#align is_semisimple_iff_top_eq_Sup_simples is_semisimple_iff_top_eq_sSup_simples
+  ⟨.of_sSup_simples_eq_top, fun _ ↦ IsSemisimpleModule.sSup_simples_eq_top⟩
+#align is_semisimple_iff_top_eq_Sup_simples sSup_simples_eq_top_iff_isSemisimpleModule
+@[deprecated]
+alias is_semisimple_iff_top_eq_sSup_simples := sSup_simples_eq_top_iff_isSemisimpleModule
 
+/-- A module generated by semisimple submodules is itself semisimple. -/
 lemma isSemisimpleModule_of_isSemisimpleModule_submodule {s : Set ι} {p : ι → Submodule R M}
     (hp : ∀ i ∈ s, IsSemisimpleModule R (p i)) (hp' : ⨆ i ∈ s, p i = ⊤) :
     IsSemisimpleModule R M := by
@@ -148,6 +279,81 @@ lemma isSemisimpleModule_of_isSemisimpleModule_submodule' {p : ι → Submodule
     IsSemisimpleModule R M :=
   isSemisimpleModule_of_isSemisimpleModule_submodule (s := Set.univ) (fun i _ ↦ hp i) (by simpa)
 
+theorem IsSemisimpleModule.sup {p q : Submodule R M}
+    (_ : IsSemisimpleModule R p) (_ : IsSemisimpleModule R q) :
+    IsSemisimpleModule R ↥(p ⊔ q) := by
+  let f : Bool → Submodule R M := Bool.rec q p
+  rw [show p ⊔ q = ⨆ i ∈ Set.univ, f i by rw [iSup_univ, iSup_bool_eq]]
+  exact isSemisimpleModule_biSup_of_isSemisimpleModule_submodule (by rintro (_|_) _ <;> assumption)
+
+instance IsSemisimpleRing.isSemisimpleModule [IsSemisimpleRing R] : IsSemisimpleModule R M :=
+  have : IsSemisimpleModule R (M →₀ R) := isSemisimpleModule_of_isSemisimpleModule_submodule'
+    (fun _ ↦ .congr (LinearMap.quotKerEquivRange _).symm) Finsupp.iSup_lsingle_range
+  .congr (LinearMap.quotKerEquivOfSurjective _ <| Finsupp.total_id_surjective R M).symm
+
+open LinearMap in
+/-- A finite product of semisimple rings is semisimple. -/
+instance {ι} [Finite ι] (R : ι → Type*) [∀ i, Ring (R i)] [∀ i, IsSemisimpleRing (R i)] :
+    IsSemisimpleRing (∀ i, R i) := by
+  letI (i) : Module (∀ i, R i) (R i) := Module.compHom _ (Pi.evalRingHom R i)
+  let e (i) : R i →ₛₗ[Pi.evalRingHom R i] R i :=
+    { AddMonoidHom.id (R i) with map_smul' := fun _ _ ↦ rfl }
+  have (i) : IsSemisimpleModule (∀ i, R i) (R i) :=
+    ((e i).isSemisimpleModule_iff_of_bijective Function.bijective_id).mpr inferInstance
+  classical
+  exact isSemisimpleModule_of_isSemisimpleModule_submodule' (p := (range <| single ·))
+    (fun i ↦ .range _) (by simp_rw [range_eq_map, Submodule.iSup_map_single, Submodule.pi_top])
+
+/-- A binary product of semisimple rings is semisimple. -/
+instance [hR : IsSemisimpleRing R] [hS : IsSemisimpleRing S] : IsSemisimpleRing (R × S) := by
+  letI : Module (R × S) R := Module.compHom _ (.fst R S)
+  letI : Module (R × S) S := Module.compHom _ (.snd R S)
+  -- e₁, e₂ got falsely flagged by the unused argument linter
+  let _e₁ : R →ₛₗ[.fst R S] R := { AddMonoidHom.id R with map_smul' := fun _ _ ↦ rfl }
+  let _e₂ : S →ₛₗ[.snd R S] S := { AddMonoidHom.id S with map_smul' := fun _ _ ↦ rfl }
+  rw [IsSemisimpleRing, ← _e₁.isSemisimpleModule_iff_of_bijective Function.bijective_id] at hR
+  rw [IsSemisimpleRing, ← _e₂.isSemisimpleModule_iff_of_bijective Function.bijective_id] at hS
+  rw [IsSemisimpleRing, ← Submodule.topEquiv.isSemisimpleModule_iff_of_bijective
+    (LinearEquiv.bijective _), ← LinearMap.sup_range_inl_inr]
+  exact .sup (.range _) (.range _)
+
+theorem RingHom.isSemisimpleRing_of_surjective (f : R →+* S) (hf : Function.Surjective f)
+    [IsSemisimpleRing R] : IsSemisimpleRing S := by
+  letI : Module R S := Module.compHom _ f
+  haveI : RingHomSurjective f := ⟨hf⟩
+  let e : S →ₛₗ[f] S := { AddMonoidHom.id S with map_smul' := fun _ _ ↦ rfl }
+  rw [IsSemisimpleRing, ← e.isSemisimpleModule_iff_of_bijective Function.bijective_id]
+  infer_instance
+
+theorem IsSemisimpleRing.ideal_eq_span_idempotent [IsSemisimpleRing R] (I : Ideal R) :
+    ∃ e : R, IsIdempotentElem e ∧ I = .span {e} := by
+  obtain ⟨J, h⟩ := exists_isCompl I
+  obtain ⟨f, idem, rfl⟩ := I.isIdempotentElemEquiv.symm (I.isComplEquivProj ⟨J, h⟩)
+  exact ⟨f 1, LinearMap.isIdempotentElem_apply_one_iff.mpr idem, by
+    erw [LinearMap.range_eq_map, ← Ideal.span_one, LinearMap.map_span, Set.image_singleton]; rfl⟩
+
+instance [IsSemisimpleRing R] : IsPrincipalIdealRing R where
+  principal I := have ⟨e, _, he⟩ := IsSemisimpleRing.ideal_eq_span_idempotent I; ⟨e, he⟩
+
+variable (ι R)
+
+proof_wanted IsSemisimpleRing.mulOpposite [IsSemisimpleRing R] : IsSemisimpleRing Rᵐᵒᵖ
+
+proof_wanted IsSemisimpleRing.module_end [IsSemisimpleRing R] [Module.Finite R M] :
+    IsSemisimpleRing (Module.End R M)
+
+proof_wanted IsSemisimpleRing.matrix [Fintype ι] [DecidableEq ι] [IsSemisimpleRing R] :
+    IsSemisimpleRing (Matrix ι ι R)
+
+universe u in
+/- The existence part of the Artin–Wedderburn theorem. -/
+proof_wanted isSemisimpleRing_iff_pi_matrix_divisionRing {R : Type u} [Ring R] :
+    IsSemisimpleRing R ↔
+    ∃ (n : ℕ) (S : Fin n → Type u) (d : Fin n → ℕ) (_ : ∀ i, DivisionRing (S i)),
+      Nonempty (R ≃+* ∀ i, Matrix (Fin (d i)) (Fin (d i)) (S i))
+
+variable {ι R}
+
 namespace LinearMap
 
 theorem injective_or_eq_zero [IsSimpleModule R M] (f : M →ₗ[R] N) :
@@ -174,11 +380,8 @@ theorem surjective_of_ne_zero [IsSimpleModule R N] {f : M →ₗ[R] N} (h : f 
 
 /-- **Schur's Lemma** for linear maps between (possibly distinct) simple modules -/
 theorem bijective_or_eq_zero [IsSimpleModule R M] [IsSimpleModule R N] (f : M →ₗ[R] N) :
-    Function.Bijective f ∨ f = 0 := by
-  by_cases h : f = 0
-  · right
-    exact h
-  exact Or.intro_left _ ⟨injective_of_ne_zero h, surjective_of_ne_zero h⟩
+    Function.Bijective f ∨ f = 0 :=
+  or_iff_not_imp_right.mpr fun h ↦ ⟨injective_of_ne_zero h, surjective_of_ne_zero h⟩
 #align linear_map.bijective_or_eq_zero LinearMap.bijective_or_eq_zero
 
 theorem bijective_of_ne_zero [IsSimpleModule R M] [IsSimpleModule R N] {f : M →ₗ[R] N} (h : f ≠ 0) :
@@ -194,33 +397,14 @@ theorem isCoatom_ker_of_surjective [IsSimpleModule R N] {f : M →ₗ[R] N}
 
 /-- Schur's Lemma makes the endomorphism ring of a simple module a division ring. -/
 noncomputable instance _root_.Module.End.divisionRing
-    [DecidableEq (Module.End R M)] [IsSimpleModule R M] : DivisionRing (Module.End R M) :=
-  {
-    (Module.End.ring :
-      Ring
-        (Module.End R
-          M)) with
-    inv := fun f =>
-      if h : f = 0 then 0
-      else
-        LinearMap.inverse f (Equiv.ofBijective _ (bijective_of_ne_zero h)).invFun
-          (Equiv.ofBijective _ (bijective_of_ne_zero h)).left_inv
-          (Equiv.ofBijective _ (bijective_of_ne_zero h)).right_inv
-    exists_pair_ne :=
-      ⟨0, 1, by
-        haveI := IsSimpleModule.nontrivial R M
-        have h := exists_pair_ne M
-        contrapose! h
-        intro x y
-        simp_rw [ext_iff, one_apply, zero_apply] at h
-        rw [← h x, h y]⟩
-    mul_inv_cancel := by
-      intro a a0
-      change a * dite _ _ _ = 1
-      ext x
-      rw [dif_neg a0, mul_eq_comp, one_apply, comp_apply]
-      exact (Equiv.ofBijective _ (bijective_of_ne_zero a0)).right_inv x
-    inv_zero := dif_pos rfl }
+    [DecidableEq (Module.End R M)] [IsSimpleModule R M] : DivisionRing (Module.End R M) where
+  __ := Module.End.ring
+  inv f := if h : f = 0 then 0 else (LinearEquiv.ofBijective _ <| bijective_of_ne_zero h).symm
+  exists_pair_ne := ⟨0, 1, have := IsSimpleModule.nontrivial R M; zero_ne_one⟩
+  mul_inv_cancel a a0 := by
+    simp_rw [dif_neg a0]; ext
+    exact (LinearEquiv.ofBijective _ <| bijective_of_ne_zero a0).right_inv _
+  inv_zero := dif_pos rfl
 #align module.End.division_ring Module.End.divisionRing
 
 end LinearMap
diff --git a/scripts/noshake.json b/scripts/noshake.json
index dc09e1cdad5ea..e68751d78fe89 100644
--- a/scripts/noshake.json
+++ b/scripts/noshake.json
@@ -279,6 +279,7 @@
   ["Mathlib.CategoryTheory.Functor.Basic"],
   "Mathlib.Tactic.Basic": ["Std"],
   "Mathlib.Tactic.Attr.Register": ["Lean.Meta.Tactic.Simp.SimpTheorems"],
+  "Mathlib.RingTheory.SimpleModule": ["Mathlib.RingTheory.Finiteness"],
   "Mathlib.Tactic.ArithMult": ["Mathlib.Tactic.ArithMult.Init"],
   "Mathlib.RingTheory.Subsemiring.Order":
   ["Mathlib.GroupTheory.Submonoid.Order"],