English
If every component has trivial Jacobson radical, then the Jacobson radical of the product is trivial: jacobson_R(∏_i M_i) = ⊥ whenever ∀i, jacobson_R(M_i) = ⊥.
Русский
Если для каждого i радикал Якобсона модуля M_i тривиален, то радикал Якобсона их произведения тривиален: jacobson_R(∏_i M_i) = ⊥ при ∀i jacobson_R(M_i) = ⊥.
LaTeX
$$$\\forall i,\\ jacobson_R(M_i)=\\bot \\quad\\Rightarrow\\quad \\operatorname{jacobson}_R\\Big(\\prod_i M_i\\Big)=\\bot.$$$
Lean4
/-- A product of modules with trivial Jacobson radical (e.g. simple modules) also has trivial
Jacobson radical. -/
theorem jacobson_pi_eq_bot (h : ∀ i, jacobson R (M i) = ⊥) : jacobson R (Π i, M i) = ⊥ :=
le_bot_iff.mp <| (jacobson_pi_le R M).trans <| by simp_rw [h, pi_univ_bot, le_rfl]
