asIdeal_jacobson — Mathlib

English

For a two-sided ideal I, the Jacobson radical of its associated ideal equals the Jacobson radical of I, transferred via the asIdeal construction.

Русский

Для двустороннего идеала I радикал Якобсона его ассоциированного идеала равен радикалу Якобсона самого I, перенесённому через конструкцию asIdeal.

LaTeX

$$asIdeal I.jacobson = (asIdeal I).jacobson$$

Lean4

theorem asIdeal_jacobson (I : TwoSidedIdeal R) : asIdeal I.jacobson = (asIdeal I).jacobson := by ext; simp [jacobson]

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