Bennett Negative Binomial mul
ProvedD1Bound5.bennettNegativeBinomial_muldiophantine-tuplesnumber-theory
The negative-integer binomial series is the formal inverse of (1+X)^k.
Preamble
import Mathlib.RingTheory.PowerSeries.Binomial import Mathlib.Tactic.Ring
Formal statement
section
open PowerSeries
namespace D1Bound5
variable {F : Type*} [Field F] [CharZero F]
theorem _root_.D1Bound5.bennettNegativeBinomial_mul (k : ℕ) :
(1 + PowerSeries.X : PowerSeries F) ^ k * binomialSeries F (-(k : F)) = 1 := by sorry
end D1Bound5
end
Source
D1Bound5/BennettPoleSeries.lean, lines 22-26, SHA-256 d467fe1ce7d532a4e4fe7ebbe139b749331fe498c06b5ac2897ed0a4d7fa6354. Project: https://github.com/tomislav-math/d1-bound5-lean