mathlib3

a4052f90 - 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`.