Theorems · Theorem · field theory

minpoly.map_algebraMap

∀ {F : Type u_3} {E : Type u_4} {A : Type u_5} [inst : Field F] [inst_1 : Field E] [inst_2 : CommRing A]
  [inst_3 : Algebra F E] [inst_4 : Algebra E A] [inst_5 : Algebra F A] [IsScalarTower F E A] {a : A},
  IsIntegral F a →
    minpoly E a ∈ Polynomial.lifts (algebraMap F E) → Polynomial.map (algebraMap F E) (minpoly F a) = minpoly E a

If a subfield F of E contains all the coefficients of minpoly E a, then minpoly F a maps to minpoly E a via algebraMap F E.

Defined in

Mathlib.FieldTheory.Minpoly.Field

Cited by

1 results in Mathlib

Foundations

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

Assumes

FieldFieldCommRingAlgebraAlgebraAlgebraIsScalarTower