Registry · Theorem I.T16 established formalized

I.T16 — Mul Cancel Fails at Zero

0 * 1 = 0 * 2 but 1 != 2. Multiplicative left-cancellation fails when the cancelled factor is zero.

Book I Part 3 Ch. 15

Dependency Graph

Depends on (2)

I.D11 I.P18

Depended on by (1)

I.T17

Lean Formalization

Module: TauLib.BookI.Denotation.Structural

Symbol: Tau.Denotation.tauIdx_mul_cancel_fails_at_zero