le_radical

Mathlib.RingTheory.Ideal.Operations

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

English

I ≤ radical I for any ideal I.

Русский

I меньше или равно radical I для любого идеала I.

LaTeX

$$$$ I \le \operatorname{radical} I $$$$

Lean4

theorem le_radical : I ≤ radical I := fun r hri => ⟨1, (pow_one r).symm ▸ hri⟩

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

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

Разделы

Аффилиация

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