Theorems · Theorem · commutative algebra

Module.Basis.traceDual_powerBasis_eq

∀ {K : Type u_4} {L : Type u_5} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  [inst_3 : FiniteDimensional K L] [inst_4 : Algebra.IsSeparable K L] (pb : PowerBasis K L) (i : Fin pb.dim),
  pb.basis.traceDual i =
    (minpolyDiv K pb.gen).coeff ↑i / (Polynomial.aeval pb.gen) (Polynomial.derivative (minpoly K pb.gen))

The dual basis of a powerbasis {1, x, x²...} under the trace form is aᵢ / f'(x), with f being the minimal polynomial of x and f / (X - x) = ∑ aᵢxⁱ.

Defined in

Mathlib.RingTheory.Trace.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

FieldFieldAlgebraFiniteDimensionalAlgebra.IsSeparable