Is there generalized binomial theorem in Mathelib?

Stream: mathlib4

[SHAO YU]

For example:

lemma Step1 {n:ℕ}{x:ℝ } : ∑'(n:ℕ ),Ring.choose (-(1:ℝ)/2) n * ((-4:ℝ )*x)^n = (1-4*x)^((-1:ℝ )/2) := by  sorry
````

[Scott Carnahan]

I'm pretty sure we don't have that yet. Also, you may need some conditions on x (e.g., |x| < 1/4) to make the series converge.

[SHAO YU]

Scott Carnahan said:

I'm pretty sure we don't have that yet. Also, you may need some conditions on x (e.g., |x| < 1/4) to make the series converge.

OK，Thanks！