instIsReducedOfIsSemisimpleRing — Mathlib

English

The Jacobson radical of a ring annihilates every semisimple module.

Русский

Радикал Якобсона кольца аннигилирует каждый полупростой модуль.

LaTeX

$$Ring.jacobson R ≤ Module.annihilator R M$$

Lean4

instance (priority := low) (R) [CommRing R] [IsSemisimpleRing R] : IsReduced R where
  eq_zero
    _ := fun ⟨n, eq⟩ ↦
    (IsSemisimpleRing.jacobson_eq_bot R).le <|
      Ideal.mem_sInf.mpr fun I hI ↦ (Ideal.isMaximal_def.mpr hI).isPrime.mem_of_pow_mem n (eq ▸ I.zero_mem)

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