English
For cyclotomic p^(k+1) over ℚ and primitive root ζ, discr in the Rat setting equals a specific expression in totient and p-powers.
Русский
Для циклотомического p^(k+1) над ℚ и примитивного ζ дискриминант в Rat-настройке равен определённому выражению через φ(p^(k+1)) и p-степени.
LaTeX
$$$\operatorname{discr}^{\mathbb{Q}}(\text{power basis}) = (-1)^{((p^{(k+1)}).totient)/2} p^{p^k((p-1)(k+1)-1)}$$$
Lean4
/-- The integral `PowerBasis` of `𝓞 K` given by a primitive root of unity, where `K` is a `p ^ k`
cyclotomic extension of `ℚ`. -/
noncomputable def integralPowerBasis [IsCyclotomicExtension {p ^ k} ℚ K] (hζ : IsPrimitiveRoot ζ (p ^ k)) :
PowerBasis ℤ (𝓞 K) :=
(Algebra.adjoin.powerBasis' (hζ.isIntegral (NeZero.pos _))).map hζ.adjoinEquivRingOfIntegers
