Registry · Definition I.D32 established formalized

I.D32 — Set-Theoretic Operations

Union = lcm, intersection = gcd, difference via prime factorization stripping. Set operations earned from the multiplicative structure on tau-Idx.

Book I Part 8 Ch. 33

Dependency Graph

Depends on (3)

Depended on by (2)

Lean Formalization

Module: TauLib.BookI.Sets.Operations

Symbol: Tau.Sets.tau_union