feat(RingTheory/SimpleModule): kill 4 proof_wanted on semisimple rings (#31672)

Prove that
+ the opposite of a semisimple ring is semisimple,
+ the endomorphism ring of a finite semisimple module is semisimple,
+ matrix rings over a semisimple ring are semisimple (these are opposites of endomorphism rings of finite free modules);
+ finite products of matrix rings over division rings are semisimple (the easy direction of Wedderburn–Artin; the hard direction was already in mathlib).

Author: alreadydone

Mathlib/Data/Matrix/Basic.lean

@@ -790,6 +790,42 @@ open Matrix
 
 namespace Matrix
 
+section Pi
+
+variable {ι : Type*} {β : ι → Type*}
+
+/-- Matrices over a Pi type are in canonical bijection with tuples of matrices. -/
+@[simps] def piEquiv : Matrix m n (Π i, β i) ≃ Π i, Matrix m n (β i) where
+  toFun f i := f.map (· i)
+  invFun f := .of fun j k i ↦ f i j k
+  left_inv _ := rfl
+  right_inv _ := rfl
+
+/-- `piEquiv` as an `AddEquiv`. -/
+@[simps!] def piAddEquiv [∀ i, Add (β i)] : Matrix m n (Π i, β i) ≃+ Π i, Matrix m n (β i) where
+  __ := piEquiv
+  map_add' _ _ := rfl
+
+/-- `piEquiv` as a `LinearEquiv`. -/
+@[simps] def piLinearEquiv (R) [Semiring R] [∀ i, AddCommMonoid (β i)] [∀ i, Module R (β i)] :
+    Matrix m n (Π i, β i) ≃ₗ[R] Π i, Matrix m n (β i) where
+  __ := piAddEquiv
+  map_smul' _ _ := rfl
+
+/-- `piEquiv` as a `RingEquiv`. -/
+@[simps!] def piRingEquiv [∀ i, AddCommMonoid (β i)] [∀ i, Mul (β i)] [Fintype n] :
+    Matrix n n (Π i, β i) ≃+* Π i, Matrix n n (β i) where
+  __ := piAddEquiv
+  map_mul' _ _ := by ext; simp [Matrix.mul_apply]
+
+/-- `piEquiv` as an `AlgEquiv`. -/
+@[simps!] def piAlgEquiv (R) [CommSemiring R] [∀ i, Semiring (β i)] [∀ i, Algebra R (β i)]
+    [Fintype n] [DecidableEq n] : Matrix n n (Π i, β i) ≃ₐ[R] Π i, Matrix n n (β i) where
+  __ := piRingEquiv
+  commutes' := (AlgHom.mk' (piRingEquiv (β := β) (n := n)).toRingHom fun _ _ ↦ rfl).commutes
+
+end Pi
+
 section Transpose
 
 open Matrix

Mathlib/LinearAlgebra/Finsupp/Defs.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl
 -/
 import Mathlib.Algebra.Module.Equiv.Defs
+import Mathlib.Algebra.Module.LinearMap.End
 import Mathlib.Algebra.Module.Pi
 import Mathlib.Data.Finsupp.SMul
 
@@ -309,3 +310,49 @@ def Module.subsingletonEquiv (R M ι : Type*) [Semiring R] [Subsingleton R] [Add
   map_smul' r _ := (smul_zero r).symm
 
 end
+
+namespace Module.End
+
+variable (ι : Type*) {R M : Type*} [Semiring R] [AddCommMonoid M] [Module R M]
+
+/-- If `M` is an `R`-module and `ι` is a type, then an additive endomorphism of `M` that
+commutes with all `R`-endomorphisms of `M` gives rise to an additive endomorphism of `ι →₀ M`
+that commutes with all `R`-endomorphisms of `ι →₀ M`. -/
+@[simps] noncomputable def ringHomEndFinsupp :
+    End (End R M) M →+* End (End R (ι →₀ M)) (ι →₀ M) where
+  toFun f :=
+  { toFun := Finsupp.mapRange.addMonoidHom f
+    map_add' := map_add _
+    map_smul' g x := x.induction_linear (by simp)
+      (fun _ _ h h' ↦ by rw [smul_add, map_add, h, h', map_add, smul_add]) fun i m ↦ by
+        ext j
+        change f (Finsupp.lapply j ∘ₗ g ∘ₗ Finsupp.lsingle i • m) = _
+        rw [map_smul]
+        simp }
+  map_one' := by ext; simp
+  map_mul' _ _ := by ext; simp
+  map_zero' := by ext; simp
+  map_add' _ _ := by ext; simp
+
+variable {ι}
+
+/-- If `M` is an `R`-module and `ι` is an nonempty type, then every additive endomorphism
+of `ι →₀ M` that commutes with all `R`-endomorphisms of `ι →₀ M` comes from an additive
+endomorphism of `M` that commutes with all `R`-endomorphisms of `M`.
+See (15) in F4 of §28 on p.131 of [Lorenz2008]. -/
+@[simps!] noncomputable def ringEquivEndFinsupp (i : ι) :
+    End (End R M) M ≃+* End (End R (ι →₀ M)) (ι →₀ M) where
+  __ := ringHomEndFinsupp ι
+  invFun f :=
+  { toFun m := f (Finsupp.single i m) i
+    map_add' _ _ := by simp
+    map_smul' g m := let g := Finsupp.mapRange.linearMap g
+      show _ = g _ i by rw [← End.smul_def g, ← map_smul]; simp [g] }
+  left_inv _ := by ext; simp
+  right_inv f := by
+    ext x j
+    change f (Finsupp.lsingle (R := R) (M := M) i ∘ₗ Finsupp.lapply j • x) i = _
+    rw [map_smul]
+    simp
+
+end Module.End

Mathlib/RingTheory/Artinian/Module.lean

@@ -6,6 +6,7 @@ Authors: Chris Hughes
 import Mathlib.Algebra.Group.Units.Opposite
 import Mathlib.Algebra.Regular.Opposite
 import Mathlib.Data.SetLike.Fintype
+import Mathlib.LinearAlgebra.FreeModule.Finite.Basic
 import Mathlib.Order.Filter.EventuallyConst
 import Mathlib.RingTheory.Ideal.Prod
 import Mathlib.RingTheory.Ideal.Quotient.Operations
@@ -440,6 +441,12 @@ theorem IsArtinianRing.of_finite (R S) [Ring R] [Ring S] [Module R S] [IsScalarT
     [IsArtinianRing R] [Module.Finite R S] : IsArtinianRing S :=
   isArtinian_of_tower R isArtinian_of_fg_of_artinian'
 
+instance (n R) [Fintype n] [DecidableEq n] [Ring R] [IsNoetherianRing R] :
+    IsNoetherianRing (Matrix n n R) := .of_finite R _
+
+instance (n R) [Fintype n] [DecidableEq n] [Ring R] [IsArtinianRing R] :
+    IsArtinianRing (Matrix n n R) := .of_finite R _
+
 /-- 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]

Mathlib/RingTheory/SimpleModule/Basic.lean

@@ -68,6 +68,9 @@ instance (R) [DivisionRing R] : IsSimpleModule R R where
 /-- A ring is semisimple if it is semisimple as a module over itself. -/
 abbrev IsSemisimpleRing := IsSemisimpleModule R R
 
+instance (priority := low) [Subsingleton R] : IsSemisimpleRing R :=
+  (isSemisimpleModule_iff R R).mpr Subsingleton.instComplementedLattice
+
 variable {R S} in
 theorem RingEquiv.isSemisimpleRing (e : R ≃+* S) [IsSemisimpleRing R] : IsSemisimpleRing S where
   __ := (Submodule.orderIsoMapComap e.toSemilinearEquiv).complementedLattice
@@ -229,6 +232,14 @@ theorem eq_bot_or_exists_simple_le (N : Submodule R M) [IsSemisimpleModule R N]
 
 variable [IsSemisimpleModule R M]
 
+theorem exists_submodule_linearEquiv_quotient (N : Submodule R M) :
+    ∃ (P : Submodule R M), Nonempty (P ≃ₗ[R] M ⧸ N) :=
+  have ⟨P, compl⟩ := exists_isCompl N; ⟨P, ⟨(N.quotientEquivOfIsCompl P compl).symm⟩⟩
+
+theorem exists_quotient_linearEquiv_submodule (N : Submodule R M) :
+    ∃ (P : Submodule R M), Nonempty (N ≃ₗ[R] M ⧸ P) :=
+  have ⟨P, compl⟩ := exists_isCompl N; ⟨P, ⟨(P.quotientEquivOfIsCompl N compl.symm).symm⟩⟩
+
 theorem extension_property {P} [AddCommGroup P] [Module R P] (f : N →ₗ[R] M)
     (hf : Function.Injective f) (g : N →ₗ[R] P) :
     ∃ h : M →ₗ[R] P, h ∘ₗ f = g :=
@@ -282,12 +293,12 @@ theorem of_injective (f : N →ₗ[R] M) (hf : Function.Injective f) : IsSemisim
   congr (Submodule.topEquiv.symm.trans <| Submodule.equivMapOfInjective f hf _)
 
 instance quotient : IsSemisimpleModule R (M ⧸ m) :=
-  have ⟨P, compl⟩ := exists_isCompl m
-  .congr (m.quotientEquivOfIsCompl P compl)
+  have ⟨_, ⟨e⟩⟩ := exists_submodule_linearEquiv_quotient m
+  .congr e.symm
 
 instance (priority := low) [Module.Finite R M] : IsNoetherian R M where
-  noetherian m := have ⟨P, compl⟩ := exists_isCompl m
-    Module.Finite.iff_fg.mp (Module.Finite.equiv <| P.quotientEquivOfIsCompl m compl.symm)
+  noetherian m := have ⟨_, ⟨e⟩⟩ := exists_quotient_linearEquiv_submodule m
+    Module.Finite.iff_fg.mp (Module.Finite.equiv e.symm)
 
 -- does not work as an instance, not sure why
 protected theorem range (f : M →ₗ[R] N) : IsSemisimpleModule R (range f) :=
@@ -397,6 +408,13 @@ theorem IsSemisimpleModule.sup {p q : Submodule R M}
   exact isSemisimpleModule_biSup_of_isSemisimpleModule_submodule
     (by rintro (_ | _) _ <;> assumption)
 
+variable (R M) in
+theorem IsSemisimpleRing.exists_linearEquiv_ideal_of_isSimpleModule [IsSemisimpleRing R]
+    [h : IsSimpleModule R M] : ∃ I : Ideal R, Nonempty (M ≃ₗ[R] I) :=
+  have ⟨J, _, ⟨e⟩⟩ := isSimpleModule_iff_quot_maximal.mp h
+  have ⟨I, ⟨e'⟩⟩ := IsSemisimpleModule.exists_submodule_linearEquiv_quotient J
+  ⟨I, ⟨e.trans e'.symm⟩⟩
+
 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
@@ -449,25 +467,6 @@ theorem IsSemisimpleRing.ideal_eq_span_idempotent [IsSemisimpleRing R] (I : Idea
 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 [IsSemisimpleModule R M] [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) :
@@ -522,6 +521,12 @@ noncomputable instance _root_.Module.End.instDivisionRing
   qsmul := _
   qsmul_def := fun _ _ => rfl
 
+instance (R) [DivisionRing R] [Module R M] [Nontrivial M] : IsSimpleModule (Module.End R M) M :=
+  isSimpleModule_iff_toSpanSingleton_surjective.mpr <| .intro ‹_› fun v hv w ↦
+    have ⟨f, eq⟩ := IsSemisimpleModule.extension_property _
+      (ker_eq_bot.mp (ker_toSpanSingleton R M hv)) (toSpanSingleton R M w)
+    ⟨f, by simpa using congr($eq 1)⟩
+
 end LinearMap
 
 namespace JordanHolderModule

Mathlib/RingTheory/SimpleModule/Isotypic.lean

@@ -71,7 +71,17 @@ theorem IsIsotypicOfType.of_isSimpleModule [IsSimpleModule R M] : IsIsotypicOfTy
     rw [isSimpleModule_iff_isAtom, isAtom_iff_eq_top] at hS
     exact ⟨.trans (.ofEq _ _ hS) Submodule.topEquiv⟩
 
-variable {R M N S}
+variable {R}
+
+theorem IsIsotypic.of_self [IsSemisimpleRing R] (h : IsIsotypic R R) : IsIsotypic R M :=
+  fun m _ m' _ ↦
+    have ⟨_, ⟨e⟩⟩ := IsSemisimpleRing.exists_linearEquiv_ideal_of_isSimpleModule R m
+    have ⟨_, ⟨e'⟩⟩ := IsSemisimpleRing.exists_linearEquiv_ideal_of_isSimpleModule R m'
+    have := IsSimpleModule.congr e.symm
+    have := IsSimpleModule.congr e'.symm
+    ⟨e'.trans <| (h _ _).some.trans e.symm⟩
+
+variable {M N S}
 
 theorem IsIsotypicOfType.of_linearEquiv_type (h : IsIsotypicOfType R M S) (e : S ≃ₗ[R] N) :
     IsIsotypicOfType R M N := fun m _ ↦ ⟨(h m).some.trans e⟩

Mathlib/RingTheory/SimpleModule/WedderburnArtin.lean

@@ -3,9 +3,11 @@ Copyright (c) 2025 Junyan Xu. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Junyan Xu
 -/
+import Mathlib.LinearAlgebra.FreeModule.Finite.Basic
 import Mathlib.RingTheory.FiniteLength
 import Mathlib.RingTheory.SimpleModule.Isotypic
 import Mathlib.RingTheory.SimpleRing.Congr
+import Mathlib.RingTheory.SimpleRing.Matrix
 
 /-!
 # Wedderburn–Artin Theorem
@@ -70,18 +72,18 @@ namespace IsSimpleRing
 
 variable (R) [IsSimpleRing R] [IsArtinianRing R]
 
-theorem isIsotypic : IsIsotypic R R :=
-  (isSimpleRing_isArtinianRing_iff.mp ⟨‹_›, ‹_›⟩).2.1
-
 instance (priority := low) : IsSemisimpleRing R :=
   (isSimpleRing_isArtinianRing_iff.mp ⟨‹_›, ‹_›⟩).1
 
+theorem isIsotypic (M) [AddCommGroup M] [Module R M] : IsIsotypic R M :=
+  (isSimpleRing_isArtinianRing_iff.mp ⟨‹_›, ‹_›⟩).2.1.of_self M
+
 /-- The **Wedderburn–Artin Theorem**: an Artinian simple ring is isomorphic to a matrix
 ring over the opposite of the endomorphism ring of its simple module. -/
 theorem exists_ringEquiv_matrix_end_mulOpposite :
     ∃ (n : ℕ) (_ : NeZero n) (I : Ideal R) (_ : IsSimpleModule R I),
       Nonempty (R ≃+* Matrix (Fin n) (Fin n) (Module.End R I)ᵐᵒᵖ) := by
-  have ⟨n, hn, S, hS, ⟨e⟩⟩ := (isIsotypic R).linearEquiv_fun
+  have ⟨n, hn, S, hS, ⟨e⟩⟩ := (isIsotypic R R).linearEquiv_fun
   refine ⟨n, hn, S, hS, ⟨.trans (.opOp R) <| .trans (.op ?_) (.symm .mopMatrix)⟩⟩
   exact .trans (.moduleEndSelf R) <| .trans e.conjRingEquiv (endVecRingEquivMatrixEnd ..)
 
@@ -98,7 +100,7 @@ to a matrix algebra over the opposite of the endomorphism algebra of its simple
 theorem exists_algEquiv_matrix_end_mulOpposite :
     ∃ (n : ℕ) (_ : NeZero n) (I : Ideal R) (_ : IsSimpleModule R I),
       Nonempty (R ≃ₐ[R₀] Matrix (Fin n) (Fin n) (Module.End R I)ᵐᵒᵖ) := by
-  have ⟨n, hn, S, hS, ⟨e⟩⟩ := (isIsotypic R).linearEquiv_fun
+  have ⟨n, hn, S, hS, ⟨e⟩⟩ := (isIsotypic R R).linearEquiv_fun
   refine ⟨n, hn, S, hS, ⟨.trans (.opOp R₀ R) <| .trans (.op ?_) (.symm .mopMatrix)⟩⟩
   exact .trans (.moduleEndSelf R₀) <| .trans (e.algConj R₀) (endVecAlgEquivMatrixEnd ..)
 
@@ -126,10 +128,11 @@ namespace IsSemisimpleModule
 
 open Module (End)
 
-variable (R) (M : Type*) [AddCommGroup M] [Module R₀ M] [Module R M] [IsScalarTower R₀ R M]
+universe v
+variable (R) (M : Type v) [AddCommGroup M] [Module R₀ M] [Module R M] [IsScalarTower R₀ R M]
   [IsSemisimpleModule R M] [Module.Finite R M]
 
-theorem exists_end_algEquiv :
+theorem exists_end_algEquiv_pi_matrix_end :
     ∃ (n : ℕ) (S : Fin n → Submodule R M) (d : Fin n → ℕ),
       (∀ i, IsSimpleModule R (S i)) ∧ (∀ i, NeZero (d i)) ∧
       Nonempty (End R M ≃ₐ[R₀] Π i, Matrix (Fin (d i)) (Fin (d i)) (End R (S i))) := by
@@ -139,11 +142,33 @@ theorem exists_end_algEquiv :
     (.piCongrRight fun c ↦ ((e c).some.algConj R₀).trans (endVecAlgEquivMatrixEnd ..)) <|
     (.piCongrLeft' R₀ _ (Finite.equivFin _))⟩⟩
 
-theorem exists_end_ringEquiv :
+theorem exists_end_ringEquiv_pi_matrix_end :
     ∃ (n : ℕ) (S : Fin n → Submodule R M) (d : Fin n → ℕ),
       (∀ i, IsSimpleModule R (S i)) ∧ (∀ i, NeZero (d i)) ∧
       Nonempty (End R M ≃+* Π i, Matrix (Fin (d i)) (Fin (d i)) (End R (S i))) :=
-  have ⟨n, S, d, hS, hd, ⟨e⟩⟩ := exists_end_algEquiv ℕ R M; ⟨n, S, d, hS, hd, ⟨e⟩⟩
+  have ⟨n, S, d, hS, hd, ⟨e⟩⟩ := exists_end_algEquiv_pi_matrix_end ℕ R M; ⟨n, S, d, hS, hd, ⟨e⟩⟩
+
+@[deprecated (since := "2025-11-16")] alias exists_end_algEquiv := exists_end_algEquiv_pi_matrix_end
+@[deprecated (since := "2025-11-16")]
+alias exists_end_ringEquiv := exists_end_ringEquiv_pi_matrix_end
+
+-- TODO: can also require D be in `Type u`, since every simple module is the quotient by an ideal.
+theorem exists_end_algEquiv_pi_matrix_divisionRing :
+    ∃ (n : ℕ) (D : Fin n → Type v) (d : Fin n → ℕ) (_ : ∀ i, DivisionRing (D i))
+      (_ : ∀ i, Algebra R₀ (D i)), (∀ i, NeZero (d i)) ∧
+      Nonempty (End R M ≃ₐ[R₀] Π i, Matrix (Fin (d i)) (Fin (d i)) (D i)) := by
+  have ⟨n, S, d, _, hd, ⟨e⟩⟩ := exists_end_algEquiv_pi_matrix_end R₀ R M
+  classical exact ⟨n, _, d, inferInstance, inferInstance, hd, ⟨e⟩⟩
+
+theorem exists_end_ringEquiv_pi_matrix_divisionRing :
+    ∃ (n : ℕ) (D : Fin n → Type v) (d : Fin n → ℕ) (_ : ∀ i, DivisionRing (D i)),
+      (∀ i, NeZero (d i)) ∧ Nonempty (End R M ≃+* Π i, Matrix (Fin (d i)) (Fin (d i)) (D i)) :=
+  have ⟨n, D, d, _, _, hd, ⟨e⟩⟩ := exists_end_algEquiv_pi_matrix_divisionRing ℕ R M
+  ⟨n, D, d, _, hd, ⟨e⟩⟩
+
+theorem _root_.IsSemisimpleRing.moduleEnd : IsSemisimpleRing (Module.End R M) :=
+  have ⟨_, _, _, _, _, ⟨e⟩⟩ := exists_end_ringEquiv_pi_matrix_divisionRing R M
+  e.symm.isSemisimpleRing
 
 end IsSemisimpleModule
 
@@ -157,7 +182,7 @@ theorem exists_algEquiv_pi_matrix_end_mulOpposite :
     ∃ (n : ℕ) (S : Fin n → Ideal R) (d : Fin n → ℕ),
       (∀ i, IsSimpleModule R (S i)) ∧ (∀ i, NeZero (d i)) ∧
       Nonempty (R ≃ₐ[R₀] Π i, Matrix (Fin (d i)) (Fin (d i)) (Module.End R (S i))ᵐᵒᵖ) :=
-  have ⟨n, S, d, hS, hd, ⟨e⟩⟩ := IsSemisimpleModule.exists_end_algEquiv R₀ R R
+  have ⟨n, S, d, hS, hd, ⟨e⟩⟩ := IsSemisimpleModule.exists_end_algEquiv_pi_matrix_end R₀ R R
   ⟨n, S, d, hS, hd, ⟨.trans (.opOp R₀ R) <| .trans (.op <| .trans (.moduleEndSelf R₀) e) <|
     .trans (.piMulOpposite _ _) (.piCongrRight fun _ ↦ .symm .mopMatrix)⟩⟩
 
@@ -200,4 +225,34 @@ theorem exists_ringEquiv_pi_matrix_divisionRing :
   have ⟨n, D, d, _, _, hd, ⟨e⟩⟩ := exists_algEquiv_pi_matrix_divisionRing ℕ R
   ⟨n, D, d, _, hd, ⟨e⟩⟩
 
+instance (n) [Fintype n] [DecidableEq n] : IsSemisimpleRing (Matrix n n R) :=
+  (isEmpty_or_nonempty n).elim (fun _ ↦ inferInstance) fun _ ↦
+    have ⟨_, _, _, _, _, ⟨e⟩⟩ := exists_ringEquiv_pi_matrix_divisionRing R
+    (e.mapMatrix (m := n).trans Matrix.piRingEquiv).symm.isSemisimpleRing
+
+instance [IsSemisimpleRing R] : IsSemisimpleRing Rᵐᵒᵖ :=
+  have ⟨_, _, _, _, _, ⟨e⟩⟩ := exists_ringEquiv_pi_matrix_divisionRing R
+  ((e.op.trans (.piMulOpposite _)).trans (.piCongrRight fun _ ↦ .symm .mopMatrix)).symm
+    |>.isSemisimpleRing
+
 end IsSemisimpleRing
+
+theorem isSemisimpleRing_mulOpposite_iff : IsSemisimpleRing Rᵐᵒᵖ ↔ IsSemisimpleRing R :=
+  ⟨fun _ ↦ (RingEquiv.opOp R).symm.isSemisimpleRing, fun _ ↦ inferInstance⟩
+
+/-- The existence part of the Artin–Wedderburn theorem. -/
+theorem isSemisimpleRing_iff_pi_matrix_divisionRing : IsSemisimpleRing R ↔
+    ∃ (n : ℕ) (D : Fin n → Type u) (d : Fin n → ℕ) (_ : Π i, DivisionRing (D i)),
+      Nonempty (R ≃+* Π i, Matrix (Fin (d i)) (Fin (d i)) (D i)) where
+  mp _ := have ⟨n, D, d, _, _, e⟩ := IsSemisimpleRing.exists_ringEquiv_pi_matrix_divisionRing R
+    ⟨n, D, d, _, e⟩
+  mpr := fun ⟨_, _, _, _, ⟨e⟩⟩ ↦ e.symm.isSemisimpleRing
+
+-- Need left-right symmetry of Jacobson radical
+proof_wanted IsSemiprimaryRing.mulOpposite [IsSemiprimaryRing R] : IsSemiprimaryRing Rᵐᵒᵖ
+
+proof_wanted isSemiprimaryRing_mulOpposite_iff : IsSemiprimaryRing Rᵐᵒᵖ ↔ IsSemiprimaryRing R
+
+-- A left Artinian ring is right Noetherian iff it is right Artinian. To be left as an `example`.
+proof_wanted IsArtinianRing.isNoetherianRing_iff_isArtinianRing_mulOpposite
+    [IsArtinianRing R] : IsNoetherianRing Rᵐᵒᵖ ↔ IsArtinianRing Rᵐᵒᵖ