radical_pos

Mathlib.RingTheory.Radical

URI: https://scilib.ai/kg/mathlib#Nat.radical_pos

English

The radical of any natural number is positive.

Русский

Корень радикала любого натурального числа положителен.

LaTeX

$$$0 < \operatorname{radical}(n)$$$

Lean4

theorem radical_pos (n : ℕ) : 0 < radical n :=
  pos_of_ne_zero radical_ne_zero

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

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

Разделы

Аффилиация

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