A theorem about an empty module may not multiply - #2749

Closed

gHashTag wants to merge 2 commits into

Commits on Aug 28, 2026

test(lean): the count of theorems about an empty module may only fall

gHashTag
and
claude
committed
e232a7c
docs(now): vacuous-theorem ratchet, and nobody builds the proofs

gHashTag
and
claude
committed
216b6a9