powerBasis — Mathlib

English

For irreducible f, the powerBasis provides a canonical basis for AdjoinRoot f with generator root f and dimension equal to deg f.

Русский

Для ирредуцируемого f базис powerBasis предоставляет канонический базис AdjoinRoot f с генератором root f и размерностью deg f.

LaTeX

$$powerBasis hf is a PowerBasis for AdjoinRoot f$$

Lean4

/-- The power basis `1, root f, ..., root f ^ (d - 1)` for `AdjoinRoot f`,
where `f` is an irreducible polynomial over a field of degree `d`. -/
@[simps!]
def powerBasis (hf : f ≠ 0) : PowerBasis K (AdjoinRoot f)
    where
  gen := root f
  dim := f.natDegree
  basis := powerBasisAux hf
  basis_eq_pow := by simp [powerBasisAux]

Похожие утверждения