English
If p is prime and IsCyclotomicExtension {p^k} K L holds, then the norm of zeta(p^k) K L − 1 equals p^minFac.
Русский
Если p — простое и IsCyclotomicExtension {p^k} над K и L, то норма zeta(p^k) − 1 равна p^{minFac}.
LaTeX
$$$\operatorname{Norm}_{K}(\zeta(p^{k}) - 1) = p^{\minFac}$$$
Lean4
/-- If `p` is a prime and `IsCyclotomicExtension {p ^ k} K L`, then there are `u : ℤˣ` and
`n : ℕ` such that the discriminant of the power basis given by `ζ - 1` is `u * p ^ n`. Often this is
enough and less cumbersome to use than `IsCyclotomicExtension.Rat.discr_prime_pow'`. -/
theorem discr_prime_pow_eq_unit_mul_pow' [IsCyclotomicExtension {p ^ k} ℚ K] (hζ : IsPrimitiveRoot ζ (p ^ k)) :
∃ (u : ℤˣ) (n : ℕ), discr ℚ (hζ.subOnePowerBasis ℚ).basis = u * p ^ n :=
by
rw [hζ.discr_zeta_eq_discr_zeta_sub_one.symm]
exact discr_prime_pow_eq_unit_mul_pow hζ (cyclotomic.irreducible_rat (NeZero.pos _))
