English
If R is reduced and Artinian, then R is semisimple.
Русский
Если R редуцировано и артиново, то R полон семисемпл.
LaTeX
$$$[\text{IsReduced}(R)] \land [\text{IsArtinianRing}(R)] \Rightarrow \mathrm{IsSemisimpleRing}(R)$$$
Lean4
/-- 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 : MaximalSpectrum R, R ⧸ I.asIdeal :=
let f := MaximalSpectrum.asIdeal (R := R)
.trans
(Ideal.quotEquivOfEq <|
ext fun x ↦ by rw [PrimeSpectrum.nilradical_eq_iInf, iInf, primeSpectrum_asIdeal_range_eq]; rfl)
(Ideal.quotientInfRingEquivPiQuotient f <| fun I J h ↦
Ideal.isCoprime_iff_sup_eq.mpr <| I.2.coprime_of_ne J.2 <| fun hIJ ↦ h <| MaximalSpectrum.ext hIJ)
