Theorems · Theorem · number theory

FiniteField.algebraMap_trace_eq_sum_pow

∀ (K : Type u_1) (L : Type u_2) [inst : Field K] [inst_1 : Field L] [Finite L] [inst_3 : Algebra K L] (x : L),
  (algebraMap K L) ((Algebra.trace K L) x) = ∑ i ∈ Finset.range (Module.finrank K L), x ^ Nat.card K ^ i

An explicit formula for the trace map: trace[L/K](x) = ∑ i < [L:K], x ^ ((#K) ^ i).

Defined in

Mathlib.FieldTheory.Finite.Trace

Cited by

0 results in Mathlib

Foundations

Depth 199 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FieldFieldFiniteAlgebra