divisors_card_eq_one_iff — Mathlib

English

The divisor set has cardinality 1 if and only if n = 1.

Русский

Множество делителей имеет кардинальность 1 тогда, когда n = 1.

LaTeX

$$$ #n.divisors = 1 \iff n = 1 $$$

Lean4

@[simp]
theorem _root_.Nat.divisors_card_eq_one_iff (n : ℕ) : #n.divisors = 1 ↔ n = 1 :=
  by
  rcases eq_or_ne n 0 with rfl | hn
  · simp
  · refine ⟨fun h ↦ ?_, fun h ↦ by simp [h]⟩
    exact (card_le_one.mp h.le 1 (one_mem_divisors.mpr hn) n (n.mem_divisors_self hn)).symm

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