radical_neg_one

Mathlib.RingTheory.Radical

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

English

radical(-1) = 1 in any suitable unique factorization monoid with zero and normalization.

Русский

radical(-1) = 1 в подходящем уникальном факторизационном моноиде с нулём и нормализацией.

LaTeX

$$$\operatorname{radical}(-1) = 1$$$

Lean4

theorem radical_neg_one : radical (-1 : R) = 1 := by simp

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

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

Разделы

Аффилиация

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