Actual coefficients · quotient-column carries · empty and zero parts · Constructive arithmetic

Kummer for arbitrary finite multinomials

Prime(p) ∧ Multinomial(parts,n,z) ⇒ ∃e. vₚ(z)=e ∧ CarryCountMany(p,parts,e)

Build the finite product of actual binomial factors and prove that its exact prime valuation equals the total column-carry count in successive addition of every part.

Open the definition-aware map Read the final theorem See campaign milestone G035

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.

Exact certificate

Fully expanded arithmetic

Inspect all 841 native tactic lines and 55 actual proof prerequisites with every definition fully expanded.

Open the exact edition →

Focused route

Final dependency cone

Start at theorem MK0011 and follow only the lemmas and conservative definitions supporting multinomial_kummer_carry_valuation.

Trace prerequisites →
Zoom between mathematical scales: complete research atlas → research domain → proof family → G035 milestone → theorem and definition dependencies.
Major independently established statements: MK000E multinomial_exists · MK0012 multinomial_empty_values · MK0013 multinomial_empty_carry_count · MK0011 multinomial_kummer_carry_valuation.
Independently verified Alpha v34 checked-use theorem family: 19 dependency-curried kernel-checked theorem bodies · 55 proof prerequisites · 26 linked definitions · 48 definition-dependency arrows · 841 exact tactic lines · first admitted v27 · not Stable. The unchanged intuitionistic kernel and separately compiled Lean verifier independently accept all 1224 bundle nodes; SHA-256 c4711433c92b67d2ebeb30131669c60563c70e0464dafa851d417fb88fb21a6d.
Exact mathematical boundary: The carry relation contains actual quotient columns and carry bits, not the desired valuation. The theorem includes all finite lists and zero parts. It uses sequential binary-column carries; a separate simultaneous-grid or permutation-invariance theorem is not asserted.