sumInv_apply — Mathlib

English

The composition sumInv I M ∘ sum I M is the identity map on the appropriate direct sum, i.e., sumInv I M composed with sum I M equals id.

Русский

Компоновка sumInv I M ∘ sum I M равна тождественному отображению на прямой сумме (то есть сумма и суммаInv — обоюдные обратные).

LaTeX

$$$ (sumInv I M) \circ (sum I M) = \mathrm{Id} $$$

Lean4

@[simp]
theorem sumInv_apply (x : AdicCompletion I (⨁ j, M j)) (j : ι) : (sumInv I M x) j = map I (component R ι _ j) x :=
  by
  apply induction_on I _ x (fun x ↦ ?_)
  rfl

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