theorem proved term proof

`inv_pole_factor_at_zero`

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

formal statement (Lean)

  85theorem inv_pole_factor_at_zero (N_l : ℕ) :
  86    inv_pole_factor 0 N_l = 1 := by

Term-mode proof.

  87  unfold inv_pole_factor
  88  simp
  89
  90/-! ## Master cert -/
  91

Lean names referenced from this declaration's body.