how to def a transfrom from ℚ_[p]⟦X⟧ →ℚ_[p]⟦X⟧

Stream: new members

[Hanliu Jiang]

I hope to get a function fun T →((1+X)^(p)-1) however i cant find a tech to do it ,
noncomputable def ϕ_PS :

ℚ_[p]⟦X⟧ →ℚ_[p]⟦X⟧

| f => (mk fun n=>PowerSeries.coeff ℚ_[p] n (((PowerSeries.coeff ℚ_[p] 0 f)•1:ℚ_[p]⟦X⟧)+∑(i:Finset.range n),

(PowerSeries.coeff ℚ_[p] i f)•((1+X)^(p)-1)^i.1))

i want to do this but can you got a better way to do it?

[Notification Bot]

This topic was moved here from #announce > how to def a transfrom from ℚ_[p]⟦X⟧ →ℚ_[p]⟦X⟧ by Mario Carneiro.

[Aaron Liu]

Please post a #mwe using #backticks