instIsPrincipalIdealRingOfIsSemisimpleRing

English

If R is semisimple, then R is a principal ideal ring; every ideal is generated by a single element.

Русский

Если R полносемпло, то каждый идеал порожден одним элементом.

LaTeX

$$$[IsSemisimpleRing(R)] \\Rightarrow IsPrincipalIdealRing(R).$$$

Lean4

instance [IsSemisimpleRing R] : IsPrincipalIdealRing R where
  principal
    I :=
    have ⟨e, _, he⟩ := IsSemisimpleRing.ideal_eq_span_idempotent I;
    ⟨e, he⟩

Похожие утверждения