From c9e316d330c0d0dd7b587e4ac29f7cdcc5003adb Mon Sep 17 00:00:00 2001
From: WenrongZou <141128015+WenrongZou@users.noreply.github.com>
Date: Fri, 21 Aug 2026 11:01:27 +0800
Subject: [PATCH] =?UTF-8?q?feat:=20instance=20Finite=20(=F0=9D=92=AA[K]=20?=
 =?UTF-8?q?=E2=A7=B8=20=F0=9D=93=82[K]=20^=20n)?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 Mathlib/NumberTheory/LocalField/Basic.lean | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/Mathlib/NumberTheory/LocalField/Basic.lean b/Mathlib/NumberTheory/LocalField/Basic.lean
index 2e27508baf8db5..98ff84e5ac1b21 100644
--- a/Mathlib/NumberTheory/LocalField/Basic.lean
+++ b/Mathlib/NumberTheory/LocalField/Basic.lean
@@ -9,6 +9,7 @@ public import Mathlib.RingTheory.Valuation.DiscreteValuativeRel
 public import Mathlib.Topology.Algebra.Module.Compact
 public import Mathlib.Topology.Algebra.Valued.LocallyCompact
 public import Mathlib.Topology.Algebra.Valued.ValuativeRel
+public import Mathlib.RingTheory.Ideal.Quotient.Index
 
 /-!
 
@@ -36,6 +37,7 @@ This implies the following typeclasses via `inferInstance`
 - `ValuativeRel.IsDiscrete K`
 - `IsDiscreteValuationRing 𝒪[K]`
 - `Finite 𝓀[K]`
+- `Finite (𝒪[K] ⧸ 𝓂[K] ^ n)`
 
 Assuming we have a compatible `UniformSpace K` instance
 (e.g. via `IsTopologicalAddGroup.toUniformSpace` and `isUniformAddGroup_of_addCommGroup`) then
@@ -147,6 +149,10 @@ instance : Finite 𝓀[K] :=
   (compactSpace_iff_completeSpace_and_isDiscreteValuationRing_and_finite_residueField.mp
     (inferInstanceAs (CompactSpace 𝒪[K]))).2.2
 
+instance (n : ℕ) : Finite (𝒪[K] ⧸ 𝓂[K] ^ n) :=
+  haveI : Finite (𝒪[K] ⧸ 𝓂[K]) := inferInstanceAs (Finite 𝓀[K])
+  Ideal.finite_quotient_pow (IsNoetherian.noetherian _) n
+
 end TopologicalSpace
 
 section UniformSpace