radical_radical

Mathlib.RingTheory.Radical

URI: https://scilib.ai/kg/mathlib#UniqueFactorizationMonoid.radical_radical

English

Applying the radical twice is the same as applying it once: rad(rad(a)) = rad(a).

Русский

Повторное применение радикала не меняет результат: радикал(radical(a)) = radical(a).

LaTeX

$$$\operatorname{radical}(\operatorname{radical}(a)) = \operatorname{radical}(a)$$$

Lean4

@[simp]
theorem radical_radical : radical (radical a) = radical a :=
  radical_eq_of_primeFactors_eq primeFactors_radical

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

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

Разделы

Аффилиация

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