radical_mono

Mathlib.RingTheory.Ideal.Operations

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

English

If I ≤ J then radical I ≤ radical J.

Русский

Если I ⊆ J, то radical(I) ⊆ radical(J).

LaTeX

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

Lean4

theorem radical_mono (H : I ≤ J) : radical I ≤ radical J := fun _ ⟨n, hrni⟩ => ⟨n, H hrni⟩

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

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

Разделы

Аффилиация

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