Registry · Proposition I.P19 established formalized

I.P19 — Integral Domain

n * m = 0 iff n = 0 or m = 0. tau-Idx has no zero divisors (integral domain property). Forward direction uses positive core closure.

Book I Part 4 Ch. 16

Dependency Graph

Depends on (2)

I.P16 I.D11

Depended on by (1)

I.T17

Lean Formalization

Module: TauLib.BookI.Denotation.Structural

Symbol: Tau.Denotation.tauIdx_integral_domain