radical_le_self_iff

Mathlib.RingTheory.Radical

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

English

For every natural number n, radical(n) ≤ n if and only if n ≠ 0.

Русский

Для любого n ∈ ℕ выполняется radical(n) ≤ n тогда и только тогда, когда n ≠ 0.

LaTeX

$$$\operatorname{radical}(n) \le n \iff n \neq 0$$$

Lean4

@[simp]
theorem radical_le_self_iff {n : ℕ} : radical n ≤ n ↔ n ≠ 0 :=
  ⟨by aesop, fun h ↦ Nat.le_of_dvd (by cutsat) radical_dvd_self⟩

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

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

Разделы

Аффилиация

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