powerBasis_gen_mem_adjoin_zeta_sub_one

English

The PowerBasis is a canonical basis formed by adjoining a primitive root and its powers.

Русский

Базис мощности — канонический базис, образованный присоединением примитивного корня и его степеней.

LaTeX

$$$\text{PowerBasis}$$$

Lean4

theorem powerBasis_gen_mem_adjoin_zeta_sub_one : (hζ.powerBasis K).gen ∈ adjoin K ({ζ - 1} : Set L) :=
  by
  rw [powerBasis_gen, adjoin_singleton_eq_range_aeval, AlgHom.mem_range]
  exact ⟨X + 1, by simp⟩

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