equivCongrLeft — Mathlib

English

Reindexing terms of a direct sum via an equivalence h : ι ≃ κ yields an additive equivalence (⨁ i, β i) ≃+ (⨁ k, β (h.symm k)).

Русский

Переиндексация членов прямой суммы посредством эквивалентности h: ι ≃ κ даёт аддитивное эквивалентство

LaTeX

$$equivCongrLeft (h : ι ≃ κ) : (⨁ i, β i) ≃+ ⨁ k, β (h.symm k))$$

Lean4

/-- Reindexing terms of a direct sum. -/
def equivCongrLeft (h : ι ≃ κ) : (⨁ i, β i) ≃+ ⨁ k, β (h.symm k) :=
  { DFinsupp.equivCongrLeft h with map_add' := DFinsupp.comapDomain'_add _ h.right_inv }

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