Registry · Definition I.D33 established formalized

I.D33 — Bounded Powerset

P_tau(X) = set of all divisors of X. Always finite: |P_tau(X)| = product of (e_i + 1) over prime factorization. No Russell paradox: strict divisibility decreases value.

Book I Part 8 Ch. 34

Dependency Graph

Depends on (3)

I.D31 I.D32 I.T09

Depended on by (5)

I.D75 I.D94 I.L06 I.P12 I.T35

Lean Formalization

Module: TauLib.BookI.Sets.Powerset

Symbol: Tau.Sets.tau_divisors