p and (ζ - 1) ^ (p - 1) are associated

Let p be a prime and ζ a primitive p-th root of unity in a domain A. Evaluating the cyclotomic polynomial Φ_p = ∏ (X - η), the product over the primitive p-th roots η, at 1 gives p = ∏ (1 - η), and each 1 - η is associated to ζ - 1. Hence p is associated to (ζ - 1) ^ (p - 1). In particular every valuation of A takes the value v(ζ - 1) ^ (p - 1) at p, which is how the valuation normalised by v(p) = 1 is read off from one normalised by v(ζ - 1) = 1.

Mathlib proves this statement for the ring of integers of a p-th cyclotomic field (IsCyclotomicExtension.Rat.associated_zeta_sub_one_pow_prime); the proof here is the same, in an arbitrary domain.

Main results

• IsPrimitiveRoot.associated_sub_one_pow_prime: (ζ - 1) ^ (p - 1) is associated to p.
• IsPrimitiveRoot.valuation_natCast_eq_valuation_sub_one_pow: a valuation v ≤ 1 on A satisfies v(p) = v(ζ - 1) ^ (p - 1).

theorem IsPrimitiveRoot.associated_sub_one_pow_prime {A : Type u_1} [CommRing A] [IsDomain A] {p : ℕ} [hp : Fact (Nat.Prime p)] {ζ : A} (hζ : IsPrimitiveRoot ζ p) : Associated ((ζ - 1) ^ (p - 1)) ↑p

If ζ is a primitive p-th root of unity in a domain A and p is prime, then (ζ - 1) ^ (p - 1) is associated to p.

theorem IsPrimitiveRoot.valuation_natCast_eq_valuation_sub_one_pow {A : Type u_1} [CommRing A] [IsDomain A] {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] {p : ℕ} [Fact (Nat.Prime p)] {ζ : A} (hζ : IsPrimitiveRoot ζ p) (v : Valuation A Γ₀) (hv : ∀ (a : A), v a ≤ 1) : v ↑p = v (ζ - 1) ^ (p - 1)

If ζ is a primitive p-th root of unity in a domain A and p is prime, then every valuation v of A bounded by 1 satisfies v(p) = v(ζ - 1) ^ (p - 1).