nonempty_properDivisors — Mathlib

English

The set of proper divisors of n is nonempty exactly when n > 1.

Русский

Множество собственных делителей n непусто тогда и только тогда, когда n > 1.

LaTeX

$$$ n.properDivisors \neq \emptyset \iff 1 < n $$$

Lean4

@[simp]
theorem nonempty_properDivisors : n.properDivisors.Nonempty ↔ 1 < n :=
  ⟨fun ⟨_m, hm⟩ ↦ one_lt_of_mem_properDivisors hm, fun hn ↦ ⟨1, one_mem_properDivisors_iff_one_lt.2 hn⟩⟩

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