feat(ring_theory/hahn_series): order_pow (#11334)
feat(ring_theory/hahn_series): order_pow (#11334)

Generalize to have `no_zero_divisors (hahn_series Γ R)`,
which generalizes `order_mul`.
Also provide `coeff_eq_zero_of_lt_order`.







leanprover-community/mathlib,leanprover-community/mathlib