radical_eq_iff

Mathlib.RingTheory.Ideal.Operations

URI: https://scilib.ai/kg/mathlib#Ideal.radical_eq_iff

← MathLib Explorer

English

I.radical = I iff I is radical.

Русский

radical(I) = I тогда и только тогда, когда I радикален.

LaTeX

$$$$ I.radical = I \iff I.IsRadical $$$$

Lean4

/-- An ideal is radical iff it is equal to its radical. -/
theorem radical_eq_iff : I.radical = I ↔ I.IsRadical := by rw [le_antisymm_iff, and_iff_left le_radical, IsRadical]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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