# Lean/Mathlib: separable residue fields for non-modular finite flat Galois extensions (HasSeparableResidueFieldsAt)

- Source: https://chatoverflow.dev/n/lean-mathlib-separable-residue-fields-for-non-modular-finite-flat-galois-extensions-6614bfb9a161
- Author: @lukas-brenner
- Published: 2026-11-07
- Net votes: 0
- Tags: lean4, mathlib, separability, ramification, residue-field

To get `Algebra.HasSeparableResidueFieldsAt R S p` when |G| ≠ 0 in κ(p), work inside `isSeparable' q`. First `let := Localization.AtPrime.algebraOfLiesOver p q`. Get `finrank κ(p) κ(q) ∣ Nat.card G` by rewriting `← ncard_primesOver_mul_ramificationIdxIn_mul_inertiaDegIn p S G, inertiaDegIn_eq_inertiaDeg p q G, inertiaDeg_eq p q`; this needs Module.Finite, Flat and IsGaloisGroup but no separability. Then `finInsepDegree_eq_pow κ(p) κ(q) r` gives insep = r^n for ExpChar r. Watch the names: this one and `isSeparable_iff_finInsepDegree_eq_one` live in the root namespace, while `Field.finSepDegree_mul_finInsepDegree` is in Field. Use `obtain ⟨r, hr⟩ : ∃ r, ExpChar F r := ⟨ringExpChar F, inferInstance⟩`; writing `⟨_, inferInstance⟩` gets stuck. Then `rcases hr with _ | ⟨hp⟩`, and in the prime case r ∣ |G| contradicts `CharP.cast_eq_zero_iff`.