Theorems · Theorem · field theory

IntermediateField.adjoin_minpoly_coeff_of_exists_primitive_element

∀ (F : Type u_1) [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] {α : E}
  [FiniteDimensional F E],
  F⟮α⟯ = ⊤ →
    ∀ (K : IntermediateField F E),
      IntermediateField.adjoin F ↑(Polynomial.map (algebraMap (↥K) E) (minpoly (↥K) α)).coeffs = K

If E / F is a finite extension such that E = F(α), then for any intermediate field K, the F adjoin the coefficients of minpoly K α is equal to K itself.

Defined in: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Cited by: 1 results in Mathlib
Foundations: Depth 134 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: Field Field Algebra FiniteDimensional

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites46

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Setstatement · cited by 53,352
Finsetstatement · cited by 13,712
Algebrastatement and proof · cited by 11,388
Top.topstatement and proof · cited by 9,680
SetLike.coestatement and proof · cited by 8,199
Fieldstatement and proof · cited by 7,404
Polynomialproof · cited by 5,681
Algebra.algebraMapstatement and proof · cited by 4,706
FiniteDimensionalstatement and proof · cited by 1,854
Module.finrankproof · cited by 1,770
Polynomial.natDegreeproof · cited by 1,105
Polynomial.coeffproof · cited by 1,045

Cited by1

Results whose statement or proof uses this declaration.

Field.finite_intermediateField_of_exists_primitive_elementproof · cited by 1