feat(LocalField): instance `Finite (𝒪[K] ⧸ 𝓂[K] ^ n)` - #42994

WenrongZou wants to merge 1 commit into

feat(LocalField): instance `Finite (𝒪[K] ⧸ 𝓂[K] ^ n)`#42994
WenrongZou wants to merge 1 commit into
leanprover-community:masterfrom
WenrongZou:quot_pow

feat: instance Finite (𝒪[K] ⧸ 𝓂[K] ^ n)