powerBasis' — Mathlib

English

The PowerBasis for adjoin R {x} is obtained by transporting the canonical power basis along the isomorphism given by minpoly.equivAdjoin hx.

Русский

Базис мощности для адъюнкта по R{ x } переносится вдоль изоморфизма, заданного minpoly.equivAdjoin hx.

LaTeX

$$$\\text{Algebra.adjoin.powerBasis}'(hx) = \\text{PowerBasis.map}(\\text{AdjoinRoot.powerBasis}'(\\minpoly.monic(hx))) (\\minpoly.equivAdjoin hx)$$$

Lean4

/-- The `PowerBasis` of `adjoin R {x}` given by `x`. See `Algebra.adjoin.powerBasis` for a version
over a field. -/
def _root_.Algebra.adjoin.powerBasis' (hx : IsIntegral R x) : PowerBasis R (Algebra.adjoin R ({ x } : Set S)) :=
  PowerBasis.map (AdjoinRoot.powerBasis' (minpoly.monic hx)) (minpoly.equivAdjoin hx)

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