English
Given a basis B of S over R and a bijection e between index types with hx describing B i = x^{e i}, one obtains a PowerBasis R S.
Русский
Задано основание B базы S над R и биекция e между индексами с условием hx: B_i = x^{e i}; тогда получается PowerBasis R S.
LaTeX
$$$\\text{PowerBasis}(R,S) := \\langle x, n, B^{\\mathrm{reindex}}(e), hx \\rangle$ where $B_i = x^{e(i)}$.$$
Lean4
/-- Construct a power basis from a basis consisting of powers of an element.
-/
def _root_.Module.Basis.PowerBasis {ι : Type*} [Fintype ι] (B : Basis ι R S) {x : S} (e : ι ≃ Fin (Fintype.card ι))
(hx : ∀ i, B i = x ^ (e i : ℕ)) : PowerBasis R S :=
⟨x, Fintype.card ι, B.reindex e, fun i ↦ by simp [hx]⟩
