English
Let R be a domain and ζ an element of R which is a primitive n-th root of unity (with n > 0). Then for any x, y in R we have x^n − y^n = ∏_{μ} (x − μ y), where μ runs over all n-th roots of unity in R.
Русский
Пусть R — область, и ζ ∈ R — примитивный корень порядка n. Тогда для любых x, y ∈ R выполняется равенство x^n − y^n = ∏_{μ^n=1} (x − μ y).
LaTeX
$$$x^n - y^n = \\prod_{\\mu \\in \\nthRootsFinset n (1 : R)} (x - \\mu \\cdot y)$$$
Lean4
/-- If there is a primitive `n`th root of unity in `R`, then `X ^ n - Y ^ n = ∏ (X - μ Y)`,
where `μ` varies over the `n`-th roots of unity. -/
theorem _root_.IsPrimitiveRoot.pow_sub_pow_eq_prod_sub_mul (hpos : 0 < n) (h : IsPrimitiveRoot ζ n) :
x ^ n - y ^ n = ∏ ζ ∈ nthRootsFinset n (1 : R), (x - ζ * y) :=
by
let K := FractionRing R
apply FaithfulSMul.algebraMap_injective R K
rw [map_sub, map_pow, map_pow, map_prod]
simp_rw [map_sub, map_mul]
have h' : IsPrimitiveRoot (algebraMap R K ζ) n := h.map_of_injective <| FaithfulSMul.algebraMap_injective R K
rw [h'.pow_sub_pow_eq_prod_sub_mul_field _ _ hpos]
refine
(prod_nbij (algebraMap R K) (fun a ha ↦ map_mem_nthRootsFinset_one ha _)
(fun a _ b _ H ↦ FaithfulSMul.algebraMap_injective R K H) (fun a ha ↦ ?_) (fun _ _ ↦ rfl)).symm
have :=
Set.surj_on_of_inj_on_of_ncard_le (s := nthRootsFinset n (1 : R)) (t := nthRootsFinset n (1 : K)) _
(fun _ hr ↦ map_mem_nthRootsFinset_one hr _) (fun a _ b _ H ↦ FaithfulSMul.algebraMap_injective R K H)
(by simp [h.card_nthRootsFinset, h'.card_nthRootsFinset])
obtain ⟨x, hx, hx1⟩ := this _ ha
exact ⟨x, hx, hx1.symm⟩
