basisSpanSingleton — Mathlib

English

Let b be a Basis ι over R of S, and x ≠ 0 in S. Then there exists a Basis for span({x}) on S given by x·b_i.

Русский

Пусть b — базис модуля S над R; для x ≠ 0 существует базис для span({x}) на S, получаемый как x·b_i.

LaTeX

$$∃ b' : Basis ι R (span({x})) с b'_i = x · b_i$$

Lean4

/-- A basis on `S` gives a basis on `Ideal.span {x}`, by multiplying everything by `x`. -/
noncomputable def basisSpanSingleton (b : Basis ι R S) {x : S} (hx : x ≠ 0) : Basis ι R (span ({ x } : Set S)) :=
  b.map <|
    LinearEquiv.ofInjective (LinearMap.mulLeft R x) (mul_right_injective₀ hx) ≪≫ₗ
        LinearEquiv.ofEq _ _
          (by
            ext
            simp [mem_span_singleton', mul_comm]) ≪≫ₗ
      (Submodule.restrictScalarsEquiv R S S (Ideal.span ({ x } : Set S))).restrictScalars R

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