Theorems · Definition · field theory

IntermediateField.adjoin.powerBasis

{K : Type u} →
  [inst : Field K] →
    {L : Type u_3} → [inst_1 : Field L] → [inst_2 : Algebra K L] → {x : L} → IsIntegral K x → PowerBasis K ↥K⟮x⟯

The power basis 1, x, ..., x ^ (d - 1) for K⟮x⟯, where d is the degree of the minimal polynomial of x.

Defined in

Mathlib.FieldTheory.IntermediateField.Adjoin.Basic

Cited by

17 results in Mathlib

Foundations

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

Assumes

FieldFieldAlgebra