@[reducible, inline]

abbrev IsDirectedSet (I : Type u_1) [PartialOrder I] : Prop

@[reducible, inline]

abbrev IsAnInverseSystem {ι : Type u_1} [Preorder ι] {F : ι → Type u_2} (f : ⦃i j : ι⦄ → i ≤ j → F j → F i) : Prop

def InvLim {ι : Type u_1} [Preorder ι] (X : ι → Type u_2) (f : ⦃i j : ι⦄ → i ≤ j → X j → X i) : Set ((i : ι) → X i)

theorem InvLim.proj_compat {ι : Type u_1} [Preorder ι] {X : ι → Type u_2} {f : ⦃i j : ι⦄ → i ≤ j → X j → X i} (x : ↑(InvLim X f)) {i j : ι} (h : i ≤ j) : f h (↑x j) = ↑x i

theorem invLim_isClosed {ι : Type u_1} [Preorder ι] {X : ι → Type u_2} [(i : ι) → TopologicalSpace (X i)] [∀ (i : ι), T2Space (X i)] {f : ⦃i j : ι⦄ → i ≤ j → X j → X i} (hf : ∀ ⦃i j : ι⦄ (h : i ≤ j), Continuous (f h)) : IsClosed (InvLim X f)

theorem invLim_isCompact {ι : Type u_1} [Preorder ι] {X : ι → Type u_2} [(i : ι) → TopologicalSpace (X i)] [∀ (i : ι), T2Space (X i)] [∀ (i : ι), CompactSpace (X i)] {f : ⦃i j : ι⦄ → i ≤ j → X j → X i} (hf : ∀ ⦃i j : ι⦄ (h : i ≤ j), Continuous (f h)) : IsCompact (InvLim X f)

noncomputable def adicComplete_ringEquiv_adicCompletion (R : Type u_1) [CommRing R] (I : Ideal R) [IsAdicComplete I R] : R ≃+* AdicCompletion I R

noncomputable def dvr_ringEquiv_adicCompletion (R : Type u_1) [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] [IsAdicComplete (IsLocalRing.maximalIdeal R) R] : R ≃+* AdicCompletion (IsLocalRing.maximalIdeal R) R

theorem mem_ideal_pow_iff_evalₐ_eq_zero (R : Type u_1) [CommRing R] (I : Ideal R) (n : ℕ) (x : R) : x ∈ I ^ n ↔ (AdicCompletion.evalₐ I n) ((algebraMap R (AdicCompletion I R)) x) = 0

theorem adicComplete_ringEquiv_symm_mem_iff_evalₐ_eq_zero (R : Type u_1) [CommRing R] (I : Ideal R) [IsAdicComplete I R] (n : ℕ) (y : AdicCompletion I R) : (adicComplete_ringEquiv_adicCompletion R I).symm y ∈ I ^ n ↔ (AdicCompletion.evalₐ I n) y = 0

theorem adicComplete_topological_ringIso (R : Type u_1) [CommRing R] (I : Ideal R) [IsAdicComplete I R] : Nonempty (R ≃+* AdicCompletion I R) ∧ (∀ (n : ℕ) (x : R), x ∈ I ^ n ↔ (AdicCompletion.evalₐ I n) ((algebraMap R (AdicCompletion I R)) x) = 0) ∧ ∀ (n : ℕ) (y : AdicCompletion I R), (adicComplete_ringEquiv_adicCompletion R I).symm y ∈ I ^ n ↔ (AdicCompletion.evalₐ I n) y = 0

noncomputable def padicIntToProd {p : ℕ} [hp : Fact (Nat.Prime p)] : ℤ_[p] → (n : ℕ) → ZMod (p ^ n)

theorem padicInt_toZModPow_injective {p : ℕ} [hp : Fact (Nat.Prime p)] : Function.Injective padicIntToProd

theorem padicIntToProd_compat {p : ℕ} [hp : Fact (Nat.Prime p)] (z : ℤ_[p]) (m n : ℕ) (h : m ≤ n) : (ZMod.castHom ⋯ (ZMod (p ^ m))) (padicIntToProd z n) = padicIntToProd z m

theorem padicInt_toZModPow_surjective {p : ℕ} [hp : Fact (Nat.Prime p)] (x : (n : ℕ) → ZMod (p ^ n)) (hcompat : ∀ (m n : ℕ) (h : m ≤ n), (ZMod.castHom ⋯ (ZMod (p ^ m))) (x n) = x m) : ∃ (z : ℤ_[p]), ∀ (n : ℕ), (PadicInt.toZModPow n) z = x n

def padicInvLimSubring {p : ℕ} : Subring ((n : ℕ) → ZMod (p ^ n))

noncomputable def padicIntToInvLimRingHom {p : ℕ} [hp : Fact (Nat.Prime p)] : ℤ_[p] →+* ↥padicInvLimSubring

theorem padicIntToInvLimRingHom_bijective {p : ℕ} [hp : Fact (Nat.Prime p)] : Function.Bijective ⇑padicIntToInvLimRingHom

noncomputable def padicDigit {p : ℕ} [hp : Fact (Nat.Prime p)] (a : ℤ_[p]) (n : ℕ) : ℕ

theorem appr_succ_eq {p : ℕ} [hp : Fact (Nat.Prime p)] (a : ℤ_[p]) (n : ℕ) : a.appr (n + 1) = a.appr n + p ^ n * padicDigit a n

def digitPartialSum (p : ℕ) (b : ℕ → ℕ) : ℕ → ℕ

@[simp]

theorem digitPartialSum_succ {p : ℕ} (b : ℕ → ℕ) (n : ℕ) : digitPartialSum p b (n + 1) = digitPartialSum p b n + p ^ n * b n

theorem digitPartialSum_lt {p : ℕ} [hp : Fact (Nat.Prime p)] (b : ℕ → ℕ) (hb : ∀ (i : ℕ), b i < p) (n : ℕ) : digitPartialSum p b n < p ^ n

theorem digitPartialSum_dvd {p : ℕ} (b : ℕ → ℕ) (n : ℕ) : ↑p ^ n ∣ ↑(digitPartialSum p b (n + 1)) - ↑(digitPartialSum p b n)

noncomputable def padicIntOfDigits {p : ℕ} [hp : Fact (Nat.Prime p)] (b : ℕ → ℕ) (_hb : ∀ (i : ℕ), b i < p) : ℤ_[p]

theorem toZModPow_padicIntOfDigits {p : ℕ} [hp : Fact (Nat.Prime p)] (b : ℕ → ℕ) (hb : ∀ (i : ℕ), b i < p) (n : ℕ) : (PadicInt.toZModPow n) (padicIntOfDigits b hb) = ↑↑(digitPartialSum p b n)

theorem appr_padicIntOfDigits {p : ℕ} [hp : Fact (Nat.Prime p)] (b : ℕ → ℕ) (hb : ∀ (i : ℕ), b i < p) (n : ℕ) : (padicIntOfDigits b hb).appr n = digitPartialSum p b n

theorem padicExpansion_unique {p : ℕ} [hp : Fact (Nat.Prime p)] (a a' : ℤ_[p]) (h : ∀ (n : ℕ), padicDigit a n = padicDigit a' n) : a = a'