English
The nth cyclotomic polynomial with coefficients in R is defined as 1 if n=0, otherwise the map of an integer-coefficient lift of cyclotomic' n ℂ into R.
Русский
N-й циклотоми́ческий полином с коэффициентами в R определяется как 1, если n=0; иначе отображением целочисленного лифта cyclotomic' n ℂ в R.
LaTeX
$$$\operatorname{cyclotomic}(n,R) = \begin{cases} 1, & n=0 \\ \operatorname{map}(\operatorname{Int.castRingHom}R)(\text{the chosen lift of }\operatorname{cyclotomic}'(n,\mathbb{C})) , & n>0 \end{cases}$$$
Lean4
/-- The `n`-th cyclotomic polynomial with coefficients in `R`. -/
def cyclotomic (n : ℕ) (R : Type*) [Ring R] : R[X] :=
if h : n = 0 then 1 else map (Int.castRingHom R) (int_coeff_of_cyclotomic' (Complex.isPrimitiveRoot_exp n h)).choose
