English
For IsCyclotomicExtension {p^k} K L, there exist units u and n with discr K (hζ.powerBasis K).basis = u * p^n.
Русский
Существует единица u и показатель n such that дискриминант диск K (hζ.powerBasis K) равен u * p^n.
LaTeX
$$∃ u∈ℤˣ, ∃ n∈ℕ, discr K (hζ.powerBasis K).basis = u * p^n$$
Lean4
/-- The discriminant of the power basis given by a primitive root of unity `ζ` is the same as the
discriminant of the power basis given by `ζ - 1`. -/
theorem discr_zeta_eq_discr_zeta_sub_one (hζ : IsPrimitiveRoot ζ n) :
discr ℚ (hζ.powerBasis ℚ).basis = discr ℚ (hζ.subOnePowerBasis ℚ).basis :=
by
haveI : NumberField K := @NumberField.mk _ _ _ (IsCyclotomicExtension.finiteDimensional { n } ℚ K)
have H₁ : (aeval (hζ.powerBasis ℚ).gen) (X - 1 : ℤ[X]) = (hζ.subOnePowerBasis ℚ).gen := by simp
have H₂ : (aeval (hζ.subOnePowerBasis ℚ).gen) (X + 1 : ℤ[X]) = (hζ.powerBasis ℚ).gen := by simp
refine
discr_eq_discr_of_toMatrix_coeff_isIntegral _ (fun i j => toMatrix_isIntegral H₁ ?_ ?_ _ _) fun i j =>
toMatrix_isIntegral H₂ ?_ ?_ _ _
· exact hζ.isIntegral (NeZero.pos _)
· refine minpoly.isIntegrallyClosed_eq_field_fractions' (K := ℚ) (hζ.isIntegral (NeZero.pos _))
· exact (hζ.isIntegral (NeZero.pos _)).sub isIntegral_one
· refine minpoly.isIntegrallyClosed_eq_field_fractions' (K := ℚ) ?_
exact (hζ.isIntegral (NeZero.pos _)).sub isIntegral_one
