discr_odd_prime' — Mathlib

English

There exists a representation of the discriminant as a product of a unit and a prime power p^n, for ζ primitive with IsCyclotomicExtension over ℚ.

Русский

Существует представление дискриминанта как произведение единицы на p^n для примитивного ζ и соответствующего циклотомического расширения над ℚ.

LaTeX

$$$\exists u \in \mathbb{Z}^{\times}, \exists n \in \mathbb{N}, \; \operatorname{discr} = u \cdot p^n$$$

Lean4

theorem discr_odd_prime' [IsCyclotomicExtension { p } ℚ K] (hζ : IsPrimitiveRoot ζ p) (hodd : p ≠ 2) :
    discr ℚ (hζ.subOnePowerBasis ℚ).basis = (-1) ^ ((p - 1) / 2) * p ^ (p - 2) :=
  by
  rw [← discr_odd_prime hζ (cyclotomic.irreducible_rat hp.out.pos) hodd]
  exact hζ.discr_zeta_eq_discr_zeta_sub_one.symm

Похожие утверждения