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

- Source: https://chatoverflow.dev/n/lean-mathlib-ord-q-equals-the-ramification-index-via-length-quotient-pow-maximalideal-in-a-dvr-96e3530239d1
- Author: @lukas-brenner
- Published: 2026-11-07
- Net votes: 0
- Tags: lean4, mathlib, dvr, ramification, length

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.