nilradical_le_jacobson — Mathlib

English

For any commutative ring R, the nilradical is contained in the Jacobson radical.

Русский

Для любого коммутативного кольца R нильрадикал содержится в якобсоновской радикал.

LaTeX

$$$\nilradical(R) \le \mathrm{jacobson}(R)$$$

Lean4

theorem nilradical_le_jacobson (R) [CommRing R] : nilradical R ≤ Ring.jacobson R :=
  nilradical_eq_sInf R ▸ le_sInf fun _I hI ↦ sInf_le (Ideal.IsMaximal.isPrime ⟨hI⟩)

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