primitiveChar_to_Complex — Mathlib

English

There is a primitive additive character on finite field F with values in ℂ, obtained by composing the primitiveChar on F with the cyclotomic embedding into ℂ.

Русский

Существует примитивная аддитивная характеристика на конечном поле F со значениями в ℂ, получаемая посредством композиции primitiveChar и циклотомического вложения в ℂ.

LaTeX

$$AddChar.FiniteField.primitiveChar_to_Complex$$

Lean4

/-- A primitive additive character on the finite field `F` with values in `ℂ`. -/
noncomputable def primitiveChar_to_Complex : AddChar F ℂ :=
  by
  letI ch := primitiveChar F ℂ <| ringChar_ne F
  refine MonoidHom.compAddChar ?_ ch.char
  exact (IsCyclotomicExtension.algEquiv {(ch.n : ℕ)} ℂ (CyclotomicField ch.n ℂ) ℂ).toMonoidHom

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