Separability of completed number-field extensions

The canonical extension of completions at finite places is finite and has a characteristic-zero base. It is therefore separable. This supplies the separability hypothesis needed to apply local different and monogenicity results to the completed integer rings.

theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion_isSeparable {K : Type u_1} [Field K] [NumberField K] {L : Type u_2} [Field L] [NumberField L] [Algebra K L] (v : HeightOneSpectrum (NumberField.RingOfIntegers K)) (w : HeightOneSpectrum (NumberField.RingOfIntegers L)) [w.asIdeal.LiesOver v.asIdeal] : Algebra.IsSeparable (adicCompletion K v) (adicCompletion L w)

The canonical extension L_w / K_v of completions of number fields is separable.