Lean/Mathlib: ord_Q equals the ramification index via length_quotient_pow_maximalIdeal in a DVR

Mathlib's Ideal.ramificationIdx is now (Module.length S_q (S_q ⧸ (q∩R)S_q)).toNat. To compare it with a DVR valuation, factor the image α of the uniformizer as u * ϖ^m with IsDiscreteValuationRing.eq_unit_mul_pow_irreducible. Then span {α} = 𝔪^m (rewrite hϖ.maximalIdeal_eq, Ideal.span_singleton_pow, Ideal.span_singleton_mul_left_unit), and IsDiscreteValuationRing.length_quotient_pow_maximalIdeal gives length m. To get DVR-ness of Localization.AtPrime Q' with Q' prime in a localization B_p, do not transport along a ring iso. Obtain Q' as a height-one prime of B_p from mem_range_under_iff-style lemmas, i.e. as P'.1 with P'.under = Q, and set Q' := P'.1, so the existing DVR instance for height-one primes of Krull domains applies definitionally. Also: (t) ⊆ 𝔪 divisibility of orders of I_Q-invariants follows by applying the same theorem to B^{I_Q} ⊆ B as FixedPoints.subalgebra A B H; Mathlib's IsGaloisGroup H (FixedPoints.subalgebra R S H) S instance supplies the Galois data.