theorem proved term proof

`Z_poly_zero`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

  63theorem Z_poly_zero (a b : ℕ) : Z_poly a b 0 = 0 := by

Term-mode proof.

  64  unfold Z_poly; ring
  65
  66/-! ## Coefficient Minimality -/
  67
  68/-- The minimal choice: both terms present, minimum a + b. -/

Lean names referenced from this declaration's body.