mathlib documentation


Adjoining elements to a field #

Some lemmas on the ring generating by adjoining an element to a field.

Main statements #

noncomputable def alg_equiv.adjoin_singleton_equiv_adjoin_root_minpoly (F : Type u_1) [field F] {R : Type u_2} [comm_ring R] [algebra F R] (x : R) :

If p is the minimal polynomial of a over F then F[a] ≃ₐ[F] F[x]/(p)

theorem lift_of_splits {F : Type u_1} {K : Type u_2} {L : Type u_3} [field F] [field K] [field L] [algebra F K] [algebra F L] (s : finset K) :

If K and L are field extensions of F and we have s : finset K such that the minimal polynomial of each x ∈ s splits in L then algebra.adjoin F s embeds in L.