jacobson — Mathlib

English

The Jacobson radical of a ring R is the Jacobson radical of R considered as an R-module, i.e. jacobson R = Module.jacobson R R.

Русский

Радикал Якобсона кольца R равен радикалу Якобсона кольца, рассматриваемого как модуль над собой: jacobson R = Module.jacobson R R.

LaTeX

$$$\\operatorname{jacobson}_R = \\operatorname{Module.jacobson}_R(R).$$$

Lean4

/-- The Jacobson radical of a ring `R` is the Jacobson radical of `R` as an `R`-module. -/
-- TODO: replace all `Ideal.jacobson ⊥` by this.

abbrev jacobson : Ideal R :=
  Module.jacobson R R

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