coe_radical

Mathlib.RingTheory.GradedAlgebra.Radical

URI: https://scilib.ai/kg/mathlib#HomogeneousIdeal.coe_radical

English

Coalition of ι, σ, A, the radical equality for a homogeneous ideal holds under the coercion to ideals.

Русский

Сохранение радикала гомогенного идеала под сведение к идеалам сохраняется.

LaTeX

$$$$ (I : HomogeneousIdeal 𝒜).radical.toIdeal = I.toIdeal.radical. $$$$

Lean4

@[simp]
theorem coe_radical (I : HomogeneousIdeal 𝒜) : I.radical.toIdeal = I.toIdeal.radical :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru