PowerSeries.divXPowOrder_pow

Stream: general

[Richard Copley]

I have a branch that adds

theorem PowerSeries.divXPowOrder_pow {R : Type*}
    [Semiring R] [NoZeroDivisors R] [Nontrivial R]
    (φ : R⟦X⟧) (n : ℕ) :
  (φ ^ n).divXPowOrder = φ.divXPowOrder ^ n

(commit). The proof is by showing that docs#divXPowOrder is equal to a monoid homomorphism and using map_pow. It's a result I had need of, so it might be useful to someone else.

OK to PR?

[Ruben Van de Velde]

Yes, go ahead

[Richard Copley]

Thanks, #31331.