cyclotomic' — Mathlib

English

The modified nth cyclotomic polynomial with coefficients in R is the product over all primitive roots μ of n in R of (X - C μ).

Русский

Модифицированный циклотромический полином n-го порядка с коэффициентами в R задаётся как произведение по всем примитивным корням μ числа n в R: ∏_{μ} (X - C μ).

LaTeX

$$$\text{cyclotomic}'(n, R) = \prod_{\mu \in \operatorname{primitiveRoots}(n,R)} (X - C\mu)$$$

Lean4

/-- The modified `n`-th cyclotomic polynomial with coefficients in `R`, it is the usual cyclotomic
polynomial if there is a primitive `n`-th root of unity in `R`. -/
def cyclotomic' (n : ℕ) (R : Type*) [CommRing R] [IsDomain R] : R[X] :=
  ∏ μ ∈ primitiveRoots n R, (X - C μ)

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