powerBasis — Mathlib

English

The power basis generated by η−1 provides a natural basis for the adjoined extension.

Русский

Базис мощности, порожденный η−1, образует естественный базис при аджойном расширении.

LaTeX

$$$\text{powerBasis}_{K}(\text{subOne })$$$

Lean4

/-- The `PowerBasis` given by a primitive root `η`. -/
@[simps!]
protected noncomputable def powerBasis : PowerBasis K L :=
  -- this is purely an optimization

  letI pb := Algebra.adjoin.powerBasis <| (integral { n } K L).isIntegral ζ
  pb.map <| (Subalgebra.equivOfEq _ _ (IsCyclotomicExtension.adjoin_primitive_root_eq_top hζ)).trans Subalgebra.topEquiv

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