no goals
𝕜 : Type u
𝕜' : Type u'
E : Type v
F : Type w
G : Type x
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
p : FormalMultilinearSeries 𝕜 𝕜 E
n✝ k n : ℕ
⊢ coeff ((fslope^[k]) p) n = coeff p (n + k)
induction k generalizing p with
| zero => rfl
| succ k ih => simp [ih, add_assoc]
no goals
case zero
𝕜 : Type u
𝕜' : Type u'
E : Type v
F : Type w
G : Type x
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
n✝ n : ℕ
p : FormalMultilinearSeries 𝕜 𝕜 E
⊢ coeff ((fslope^[Nat.zero]) p) n = coeff p (n + Nat.zero)
rfl
no goals
case succ
𝕜 : Type u
𝕜' : Type u'
E : Type v
F : Type w
G : Type x
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
n✝ n k : ℕ
ih : ∀ {p : FormalMultilinearSeries 𝕜 𝕜 E}, coeff ((fslope^[k]) p) n = coeff p (n + k)
p : FormalMultilinearSeries 𝕜 𝕜 E
⊢ coeff ((fslope^[Nat.succ k]) p) n = coeff p (n + Nat.succ k)
simp [ih, add_assoc]