feat(RingTheory/RamificationInertia/Inertia): add inertiaDeg'_pos (leanprover-community#39073)

This PR adds a positivity lemma for the new `inertiaDeg'` (which will eventually replace `inertiaDeg`).

An extra import is needed to synthesize finiteness on the residue fields.

Co-authored-by: tb65536 <thomas.l.browning@gmail.com>

Author: tb65536

Mathlib/RingTheory/RamificationInertia/Inertia.lean

@@ -6,6 +6,7 @@ Authors: Thomas Browning
 module
 
 public import Mathlib.NumberTheory.RamificationInertia.Inertia
+public import Mathlib.RingTheory.QuasiFinite.Basic
 
 /-!
 # Inertia degree
@@ -54,6 +55,11 @@ theorem inertiaDeg'_def [hq : q.IsPrime]
 theorem inertiaDeg'_of_not_isPrime (hq : ¬ q.IsPrime) : q.inertiaDeg' R = 0 :=
   dif_neg hq
 
+theorem inertiaDeg'_pos [hq : q.IsPrime] [Module.Finite R S] : 0 < q.inertiaDeg' R := by
+  let := Localization.AtPrime.algebraOfLiesOver (q.under R) q
+  rw [inertiaDeg'_def]
+  apply Module.finrank_pos
+
 end
 
 section