English
The first coefficient of φ^n equals n times the first coefficient of φ times the (n−1)-st power of the constant term (for n≥1; 0 if n=0).
Русский
Первый коэффициент φ^n равен n-кратному первому коэффициенту φ, умноженному на (константный коэффициент φ)^{n−1} (при n≥1; при n=0 равно 0).
LaTeX
$$$\operatorname{coeff}_1(\phi^{n}) = n \cdot \operatorname{coeff}_1(\phi) \cdot (\operatorname{constantCoeff}(\phi))^{n-1}$$$
Lean4
/-- First coefficient of the `n`-th power of a power series. -/
theorem coeff_one_pow (n : ℕ) (φ : R⟦X⟧) : coeff 1 (φ ^ n) = n * coeff 1 φ * (constantCoeff φ) ^ (n - 1) :=
by
rcases Nat.eq_zero_or_pos n with (rfl | hn)
· simp
induction n with
| zero => cutsat
| succ n' ih =>
have h₁ (m : ℕ) : φ ^ (m + 1) = φ ^ m * φ := by exact rfl
have h₂ : Finset.antidiagonal 1 = {(0, 1), (1, 0)} := by exact rfl
rw [h₁, coeff_mul, h₂, Finset.sum_insert, Finset.sum_singleton]
· simp only [coeff_zero_eq_constantCoeff, map_pow, Nat.cast_add, Nat.cast_one, add_tsub_cancel_right]
have h₀ : n' = 0 ∨ 1 ≤ n' := by omega
rcases h₀ with h' | h'
· by_contra h''
rw [h'] at h''
simp only [pow_zero, one_mul, coeff_one, one_ne_zero, ↓reduceIte, zero_mul, add_zero, mul_one] at h''
norm_num at h''
· rw [ih]
· conv => lhs; arg 2; rw [mul_comm, ← mul_assoc]
move_mul [← constantCoeff φ ^ (n' - 1)]
conv => enter [1, 2, 1, 1, 2]; rw [← pow_one (a := constantCoeff φ)]
rw [← pow_add (a := constantCoeff φ)]
conv => enter [1, 2, 1, 1]; rw [Nat.sub_add_cancel h']
ring
exact h'
· decide
