radical — Mathlib

English

The radical of a homogeneous ideal commutes with taking the underlying ideal.

Русский

Радикал гомогенного идеала согласуется с взятием соответствующего идеала.

LaTeX

$$$$ I.radical.toIdeal = I.toIdeal.radical. $$$$

Lean4

/-- The radical of a homogeneous ideal, as another homogeneous ideal. -/
def radical (I : HomogeneousIdeal 𝒜) : HomogeneousIdeal 𝒜 :=
  ⟨I.toIdeal.radical, I.isHomogeneous.radical⟩

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