radical_neg

Mathlib.RingTheory.Radical

URI: https://scilib.ai/kg/mathlib#UniqueFactorizationDomain.radical_neg

Lean4

@[simp]
theorem radical_neg : radical (-a) = radical a :=
  radical_eq_of_associated Associated.rfl.neg_left

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

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

Разделы

Аффилиация

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