theorem KroneckerWeber.isPrimitiveRoot_mem_integralClosure {p : ℕ} [hp : Fact (Nat.Prime p)] {L : Type u_1} [Field L] [Algebra ℚ_[p] L] {ζ : L} (hζ : IsPrimitiveRoot ζ p) : ζ ∈ integralClosure ℤ_[p] L

theorem KroneckerWeber.natCast_p_mem_maximalIdeal_integralClosure (p : ℕ) [hp : Fact (Nat.Prime p)] (L : Type u_1) [Field L] [Algebra ℚ_[p] L] [IsCyclotomicExtension {p} ℚ_[p] L] : have x := ⋯; ↑p ∈ IsLocalRing.maximalIdeal ↥(integralClosure ℤ_[p] L)

theorem KroneckerWeber.residueChar_integralClosure_eq_p (p : ℕ) [hp : Fact (Nat.Prime p)] (L : Type u_1) [Field L] [Algebra ℚ_[p] L] [IsCyclotomicExtension {p} ℚ_[p] L] : have x := ⋯; ringChar (IsLocalRing.ResidueField ↥(integralClosure ℤ_[p] L)) = p

theorem KroneckerWeber.charP_residueField_integralClosure (p : ℕ) [hp : Fact (Nat.Prime p)] (L : Type u_1) [Field L] [Algebra ℚ_[p] L] [IsCyclotomicExtension {p} ℚ_[p] L] : have x := ⋯; CharP (IsLocalRing.ResidueField ↥(integralClosure ℤ_[p] L)) p

theorem KroneckerWeber.geom_sum_prod_mem_integralClosure {p : ℕ} [hp : Fact (Nat.Prime p)] {L : Type u_1} [Field L] [Algebra ℚ_[p] L] {ζ : L} (hζ : IsPrimitiveRoot ζ p) : geom_sum_prod ζ p ∈ integralClosure ℤ_[p] L