add_mul

Statement with defined notation

forall n m k. (n + m) * k = n * k + m * k

Every purple notation token opens its conservative definition. This is a reading surface; the compiler expands the statement before the unchanged kernel checks it.

Definitions used by this theorem

In the theorem statement

0 occurrences

In local proof propositions

0 occurrences

Proof neighborhood

Direct theorem prerequisites

Direct theorem dependents

Definition-aware tactic body

Only local propositions introduced by have or suffices are compacted. The untrusted compiler re-expands each one before the original tactic script is replayed; defined notation is never accepted by the kernel. Open the exact replay line beneath every changed command.