English
A finite product of semisimple rings is semisimple. More precisely, if ι is finite and each R_i is a semisimple ring, then the product ∏_{i∈ι} R_i is semisimple.
Русский
Конечное произведение полносемповых колец является полносемповым.
LaTeX
$$$\\forall \\iota\\;[\\text{Finite }\\iota],\\; (R_i)_{i\\in\\iota},\\; (\\forall i\\in\\iota),\\ IsSemisimpleRing(R_i) \\Rightarrow IsSemisimpleRing\\Bigl(\\prod_{i\\in\\iota} R_i\\Bigr).$$$
Lean4
/-- 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
infer_instance
