jacobson — Mathlib

English

The Jacobson radical of I is the intersection of all maximal ideals containing I.

Русский

Якобсонов радикал I равен пересечению всех максимальных идеалов, содержащих I.

LaTeX

$$\mathrm{jacobson}(I) = \bigcap_{J: \ I \le J \wedge \ IsMaximal J} J$$

Lean4

/-- The Jacobson radical of `I` is the infimum of all maximal (left) ideals containing `I`. -/
def jacobson (I : Ideal R) : Ideal R :=
  sInf {J : Ideal R | I ≤ J ∧ IsMaximal J}

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