PowerBasis_gen — Mathlib

English

In a PowerBasis pb, the generator equals the formal variable used to generate the basis.

Русский

В PowerBasis pb генератор равен базисному элементу, задающему все степени.

LaTeX

$$$(B.PowerBasis e hx).gen = x$$$

Lean4

@[simp]
theorem _root_.Module.Basis.PowerBasis_gen {ι : Type*} [Fintype ι] (B : Basis ι R S) {x : S}
    (e : ι ≃ Fin (Fintype.card ι)) (hx : ∀ i, B i = x ^ (e i : ℕ)) : (B.PowerBasis e hx).gen = x :=
  rfl

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