Theorems · Theorem · field theory

Field.primitive_element_inf_aux

∀ (F : Type u_1) [inst : Field F] [Infinite F] {E : Type u_2} [inst_2 : Field E] (α β : E) [inst_3 : Algebra F E]
  [Algebra.IsSeparable F E], ∃ γ, F⟮α, β⟯ = F⟮γ⟯

This is the heart of the proof of the primitive element theorem. It shows that if F is infinite and α and β are separable over F then F⟮α, β⟯ is generated by a single element.

Defined in

Mathlib.FieldTheory.PrimitiveElement

Cited by

1 results in Mathlib

Foundations

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

Assumes

FieldInfiniteFieldAlgebraAlgebra.IsSeparable