@[implicit_reducible]

noncomputable instance CyclotomicDVR.instAlgebra (p : ℕ) [hp : Fact (Nat.Prime p)] (L : Type u_1) [Field L] [Algebra ℚ_[p] L] : Algebra ℤ_[p] L

instance CyclotomicDVR.instIsScalarTower (p : ℕ) [hp : Fact (Nat.Prime p)] (L : Type u_1) [Field L] [Algebra ℚ_[p] L] : IsScalarTower ℤ_[p] ℚ_[p] L

instance CyclotomicDVR.instFiniteDimensional (p : ℕ) [hp : Fact (Nat.Prime p)] (L : Type u_1) [Field L] [Algebra ℚ_[p] L] [IsCyclotomicExtension {p} ℚ_[p] L] : FiniteDimensional ℚ_[p] L

theorem CyclotomicDVR.isLocalRing (p : ℕ) [hp : Fact (Nat.Prime p)] (L : Type u_1) [Field L] [Algebra ℚ_[p] L] [IsCyclotomicExtension {p} ℚ_[p] L] : IsLocalRing ↥(integralClosure ℤ_[p] L)

theorem CyclotomicDVR.isDVR (p : ℕ) [hp : Fact (Nat.Prime p)] (L : Type u_1) [Field L] [Algebra ℚ_[p] L] [IsCyclotomicExtension {p} ℚ_[p] L] : IsDiscreteValuationRing ↥(integralClosure ℤ_[p] L)

theorem CyclotomicDVR.isAdicComplete (p : ℕ) [hp : Fact (Nat.Prime p)] (L : Type u_1) [Field L] [Algebra ℚ_[p] L] [IsCyclotomicExtension {p} ℚ_[p] L] : IsAdicComplete (IsLocalRing.maximalIdeal ↥(integralClosure ℤ_[p] L)) ↥(integralClosure ℤ_[p] L)