divisors — Mathlib

English

The divisors of n form a Finset consisting of all positive integers d with d ∣ n and 1 ≤ d ≤ n; by convention, divisors(0) = ∅.

Русский

Делители числа n образуют конечный набор всех положительных делителей d числа n, удовлетворяющих d ∣ n и 1 ≤ d ≤ n; по соглашению divisors(0) = ∅.

LaTeX

$$$\mathrm{divisors}(n) = \{ d \in \mathbb{N} : 1 \le d \le n \ \land\ d \mid n\}$, с конвенцией $\mathrm{divisors}(0) = \emptyset$.$$

Lean4

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

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