trace_eq_finrank_mul_minpoly_nextCoeff

English

For pb a power basis of L over K, and a suitable splitting extension E, the trace's image under algebra maps equals the sum over the finitely many K-embeddings into E of pb.gen.

Русский

Для pb — степенного базиса L над K, при подходящем раскрытии в E, образ следа через алгебраическую карту равен сумме pb.gen по всем K-однозначным вложениям в E.

LaTeX

$$$\\operatorname{algebraMap}_{K,E}(\\operatorname{trace}_{K,L}(\\mathrm{gen})) = \\sum_{\\sigma \\in (L \\to_{K} E) } \\sigma(\\mathrm{gen})$$$

Lean4

theorem trace_eq_finrank_mul_minpoly_nextCoeff [FiniteDimensional K L] (x : L) :
    trace K L x = finrank K⟮x⟯ L * -(minpoly K x).nextCoeff := by
  rw [trace_eq_trace_adjoin, trace_adjoinSimpleGen (.of_finite K x), Algebra.smul_def]; rfl

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