theorem
KroneckerWeber.isPrimitiveRoot_mem_integralClosure
{p : ℕ}
[hp : Fact (Nat.Prime p)]
{L : Type u_1}
[Field L]
[Algebra ℚ_[p] L]
{ζ : L}
(hζ : IsPrimitiveRoot ζ p)
:
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.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)
: