Theorems · Definition · field theory

Field.powerBasisOfFiniteOfSeparable

(F : Type u_1) →
  (E : Type u_2) →
    [inst : Field F] →
      [inst_1 : Field E] → [inst_2 : Algebra F E] → [FiniteDimensional F E] → [Algebra.IsSeparable F E] → PowerBasis F E

Alternative phrasing of primitive element theorem: a finite separable field extension has a basis 1, α, α^2, ..., α^n. See also exists_primitive_element.

Defined in

Mathlib.FieldTheory.PrimitiveElement

Cited by

3 results in Mathlib

Foundations

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

Assumes

FieldFieldAlgebraFiniteDimensionalAlgebra.IsSeparable