constr_basisSpanSingleton — Mathlib

English

Given a basis b of S over R and x ≠ 0, the constrained basis construction yields a linear map equal to left multiplication by x on S when restricted to span({x}).

Русский

При заданном базисе b над R и x ≠ 0, конструкция constr basisSpanSingleton задаёт линейное отображение, равное левому умножению на x на S при ограничении на span({x}).

Lean4

@[simp]
theorem constr_basisSpanSingleton {N : Type*} [Semiring N] [Module N S] [SMulCommClass R N S] (b : Basis ι R S) {x : S}
    (hx : x ≠ 0) : (b.constr N).toFun (((↑) : _ → S) ∘ (basisSpanSingleton b hx)) = Algebra.lmul R S x :=
  b.ext fun i => by simp

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