sumEquivOfFintype_apply — Mathlib

English

For a finite index type ι, the sumEquivOfFintype map coincides with the direct sum map when restricted to AdicCompletion I (⨁ j, M_j).

Русский

Для конечного множества индексов ι отображение sumEquivOfFintype совпадает с прямым суммированием на AdicCompletion I (⨁ j, M_j).

LaTeX

$$$ sumEquivOfFintype I M \\ x = sum I M \\ x $$$

Lean4

@[simp]
theorem sumEquivOfFintype_apply (x : ⨁ j, (AdicCompletion I (M j))) : sumEquivOfFintype I M x = sum I M x :=
  rfl

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