English
A reduced Artinian ring is isomorphic to a finite product of fields, namely the quotients by its maximal ideals.
Русский
Редуцированное артиново кольцо изоморфно конечному произведению полей, тождественно как фактор-кубы по максимальным идеалам.
LaTeX
$$$R \cong \prod_{I \in \mathrm{MaximalSpectrum}(R)} (R/I)$, for reduced Artinian R$$
Lean4
/-- 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 : MaximalSpectrum R, R ⧸ I.asIdeal :=
.trans (.symm <| .quotientBot R) <| .trans (Ideal.quotEquivOfEq (nilradical_eq_zero R).symm) (quotNilradicalEquivPi R)
