157theorem polyCost_pow {P : Polynomial F} (hP : P ≠ 0) (k : ℕ) : 158 polyCost (P ^ k) = (k : ℝ) * polyCost P := by
proof body
Term-mode proof.
159 induction k with 160 | zero => simp [polyCost_one] 161 | succ k ih => 162 have hPk : P ^ k ≠ 0 := pow_ne_zero k hP 163 rw [pow_succ, polyCost_mul hPk hP, ih] 164 push_cast 165 ring 166 167/-- Cost is monotonic under multiplication by nonzero polynomials. -/
used by (1)
From the project-wide theorem graph. These declarations reference this one in their body.