radical_isRadical — Mathlib

English

Let I be an ideal in a commutative semiring R. Then the radical of I is a radical ideal; i.e., it satisfies the defining property of a radical ideal.

Русский

Пусть I — идеал в коммутативном полускольце R. Тогда радикал I является радикальным идеалом; то есть удовлетворяет определению радикального идеала.

LaTeX

$$$(\\operatorname{radical}(I)).IsRadical$$$

Lean4

theorem radical_isRadical : (radical I).IsRadical := fun r ⟨n, k, hrnki⟩ => ⟨n * k, (pow_mul r n k).symm ▸ hrnki⟩

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