powerBasis'_gen — Mathlib

English

The generator of the transported power basis is x, i.e. the basis is generated by x.

Русский

Генератор перенесенного базиса мощности есть x; базис генерируется x.

LaTeX

$$$(\\text{Adjoin}.\\text{powerBasis}'(hx)).\\text{gen} = \\langle x, \\text{proof that } x \\in \\text{adjoin}(R,\\{x\\})\\rangle$$$

Lean4

@[simp]
theorem _root_.Algebra.adjoin.powerBasis'_gen (hx : IsIntegral R x) :
    (adjoin.powerBasis' hx).gen = ⟨x, SetLike.mem_coe.1 <| subset_adjoin <| mem_singleton x⟩ := by
  rw [Algebra.adjoin.powerBasis', PowerBasis.map_gen, AdjoinRoot.powerBasis'_gen, equivAdjoin,
    AlgEquiv.ofBijective_apply, Minpoly.toAdjoin, liftHom_root]

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