lequivCongrLeft — Mathlib

English

Reindexing terms of a direct sum is linear: given an equivalence h: ι ≃ κ, there is a linear equivalence between ⊕_i M_i and ⊕_k M_{h^{-1}(k)}.

Русский

Переиндексация компонент прямой суммы линейно эквивалентна: существует линейное эквивалентность между ⊕_i M_i и ⊕_k M_{h^{-1}(k)}.

LaTeX

$$$\\mathrm{lequivCongrLeft}(h) : (\\bigoplus_{i} M_i) \\cong_{R} (\\bigoplus_{k} M_{h^{-1}(k)}) ,\\quad (\\mathrm{lequivCongrLeft}(h))((x_i)_i) = (x_{h^{-1}(k)})_k.$$$

Lean4

/-- Reindexing terms of a direct sum is linear. -/
def lequivCongrLeft (h : ι ≃ κ) : (⨁ i, M i) ≃ₗ[R] ⨁ k, M (h.symm k) :=
  DFinsupp.domLCongr h

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