norm_zeta_pow_sub_one_of_prime_pow_ne_two

English

If Irreducible cyclotomic, then discriminant of the zeta-based power basis equals a unit times p^n as in discr_prime_pow_eq_unit_mul_pow'.

Русский

Если циклотомическое ирреducible, дискриминант базиса, стоящего на ζ, равен единице, умноженной на p^n (соответственно discr_prime_pow_eq_unit_mul_pow').

LaTeX

$$$\operatorname{discr} \mathbb{Q}(\text{ζ}-1) = u \cdot p^n$ for some unit u and n$$$

Lean4

/-- If `Irreducible (cyclotomic (p ^ (k + 1)) K)` (in particular for `K = ℚ`) and `p` is a prime,
then the norm of `(zeta (p ^ (k + 1)) K L) ^ (p ^ s) - 1` is `p ^ (p ^ s)`
if `p ^ (k - s + 1) ≠ 2`. -/
theorem norm_zeta_pow_sub_one_of_prime_pow_ne_two {k : ℕ} [Fact p.Prime] [IsCyclotomicExtension {p ^ (k + 1)} K L]
    (hirr : Irreducible (cyclotomic (p ^ (k + 1)) K)) {s : ℕ} (hs : s ≤ k) (htwo : p ^ (k - s + 1) ≠ 2) :
    norm K (zeta (p ^ (k + 1)) K L ^ p ^ s - 1) = (p : K) ^ p ^ s :=
  (zeta_spec _ K L).norm_pow_sub_one_of_prime_pow_ne_two hirr hs htwo

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