Commit 2022-01-11 11:13 a4052f90
View on Github →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.
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.