two_le_radical_iff — Mathlib

English

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

Русский

Для любого n ∈ ℕ верно: 2 ≤ radical(n) тогда и только тогда, когда 2 ≤ n.

LaTeX

$$$2 \le \operatorname{radical}(n) \iff 2 \le n$$$

Lean4

@[simp]
theorem two_le_radical_iff {n : ℕ} : 2 ≤ radical n ↔ 2 ≤ n :=
  by
  refine ⟨?_, ?_⟩
  ·
    match n with
    | 0 | 1 | _ + 2 => simp
  · intro hn
    obtain ⟨p, hp, hpn⟩ := Nat.exists_prime_and_dvd (show n ≠ 1 by cutsat)
    trans p
    · apply hp.two_le
    · apply Nat.le_of_dvd (Nat.pos_of_ne_zero radical_ne_zero)
      rwa [dvd_radical_iff_of_irreducible hp.prime.irreducible (by cutsat)]

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