properDivisors — Mathlib

English

The proper divisors of n are the divisors of n different from n itself; by convention, properDivisors(0) = ∅.

Русский

Правильные делители n — это делители n, отличные от самого n; по соглашению properDivisors(0) = ∅.

LaTeX

$$$\mathrm{properDivisors}(n) = \{ d \in \mathbb{N} : 1 \le d < n \land d \mid n\}$$$

Lean4

/-- `properDivisors n` is the `Finset` of divisors of `n`, other than `n`.
By convention, we set `properDivisors 0 = ∅`. -/
def properDivisors : Finset ℕ :=
  {d ∈ Ico 1 n | d ∣ n}

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