term_[X]__ — Mathlib

English

If μ is a primitive nth root of unity (over rationals) then the minimal polynomial of μ divides the cyclotomic polynomial.

Русский

Если μ примитивный n-й корень единицы, то минимальный полином μ делит циклотомику.

LaTeX

$$$$ \\minpoly_{\\mathbb{Z}}(\\mu) \\mid \\operatorname{cyclotomic}(n, \\mathbb{Z}). $$$$

Lean4

@[inherit_doc Polynomial.degreeLT, scoped term_parser 1000]
public meta def «term_[X]__» : Lean.TrailingParserDescr✝ :=
  ParserDescr.trailingNode✝ `Polynomial.«term_[X]__» 9000 0
    (ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ "[X]_") (ParserDescr.cat✝ `term 1023))

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