mathlib3

88b76e4c - feat(ring_theory/valuation/valuation_subring): Add `valuation_subring.inertia_subgroup` (#17086)

feat(ring_theory/valuation/valuation_subring): Add `valuation_subring.inertia_subgroup` (#17086) The decomposition and inertia subgroups. Co-authored-by: Eric Wieser <wieser.eric@gmail.com> Co-authored-by: Michail Karatarakis <40603357+mkaratarakis@users.noreply.github.com>