collectedBasis_repr_of_mem_ne — Mathlib

English

If i ≠ j and x ∈ A_i, the coefficient at index ⟨j, a⟩ of x's collected-basis representation vanishes.

Русский

Если i ≠ j и x ∈ A_i, коэффициент при индексе ⟨j,a⟩ в представлении x относительно собранного базиса равен нулю.

LaTeX

$$$\text{collectedBasis repr}_{⟨j,a⟩}(x)=0$ for i ≠ j$$

Lean4

theorem collectedBasis_repr_of_mem_ne (h : IsInternal A) {α : ι → Type*} (v : ∀ i, Basis (α i) R (A i)) {x : M}
    {i j : ι} (hij : i ≠ j) {a : α j} (hx : x ∈ A i) : (h.collectedBasis v).repr x ⟨j, a⟩ = 0 :=
  by
  change (sigmaFinsuppLequivDFinsupp R).symm (DFinsupp.mapRange _ (fun i ↦ map_zero _) _) _ = _
  simp [h.ofBijective_coeLinearMap_of_mem_ne hij hx]

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