pow_add_pow_eq_prod_add_mul — Mathlib

English

If n is odd and ζ is a primitive n-th root of unity in a ring R, then x^n + y^n equals the product ∏_{μ^n=1} (x + μ y).

Русский

Если n нечетно и ζ — примитивный корень порядка n в кольце 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` and `n` is odd, then
`X ^ n + Y ^ n = ∏ (X + μ Y)`, where `μ` varies over the `n`-th roots of unity. -/
theorem _root_.IsPrimitiveRoot.pow_add_pow_eq_prod_add_mul (hodd : Odd n) (h : IsPrimitiveRoot ζ n) :
    x ^ n + y ^ n = ∏ ζ ∈ nthRootsFinset n (1 : R), (x + ζ * y) := by
  simpa [hodd.neg_pow] using h.pow_sub_pow_eq_prod_sub_mul x (-y) hodd.pos

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