Registry · Proposition I.P11 established formalized

I.P11 — Distributive Lattice

(tau-Idx, in_tau) forms a distributive lattice under gcd (meet) and lcm (join). Distributivity follows from the FTA.

Book I Part 8 Ch. 33

Dependency Graph

Depends on (2)

I.D32 I.D31

Lean Formalization

Module: TauLib.BookI.Sets.Operations

Symbol: Tau.Sets.tau_inter_distrib_union