Theorems · Theorem · field theory

Algebra.normalizedTrace_algebraMap_of_lifts

∀ (F : Type u_3) (E : Type u_4) (K : Type u_5) [inst : Field F] [inst_1 : Field E] [inst_2 : Field K]
  [inst_3 : Algebra F E] [inst_4 : Algebra E K] [inst_5 : Algebra F K] [IsScalarTower F E K]
  [inst_7 : Algebra.IsIntegral F K] [inst_8 : CharZero F] [inst_9 : CharZero E] [inst_10 : Algebra.IsIntegral E K]
  (a : K),
  minpoly E a ∈ Polynomial.lifts (algebraMap F E) →
    (algebraMap F E) ((Algebra.normalizedTrace F K) a) = (Algebra.normalizedTrace E K) a

If all the coefficients of minpoly E a are in F, then the normalized trace of a from K to E equals the normalized trace of a from K to F.

Defined in

Mathlib.FieldTheory.NormalizedTrace

Cited by

1 results in Mathlib

Foundations

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

Assumes

FieldFieldFieldAlgebraAlgebraAlgebraIsScalarTowerAlgebra.IsIntegralCharZeroCharZeroAlgebra.IsIntegral