primitiveChar_to_Complex_isPrimitive

English

Let F be a finite field. The complex-valued additive character associated to F that is primitive is itself primitive.

Русский

Пусть F — конечное поле. Аддитивный комплекснозначный характер, получаемый от F и являющийся примитивным, сам по себе является примитивным.

LaTeX

$$$\mathrm{IsPrimitive}(\mathrm{primitiveChar\_to\_Complex}(F))$$$

Lean4

theorem primitiveChar_to_Complex_isPrimitive : (primitiveChar_to_Complex F).IsPrimitive :=
  by
  refine IsPrimitive.compMulHom_of_isPrimitive (PrimitiveAddChar.prim _) ?_
  let nn := (primitiveChar F ℂ <| ringChar_ne F).n
  exact (IsCyclotomicExtension.algEquiv {(nn : ℕ)} ℂ (CyclotomicField nn ℂ) ℂ).injective

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