English
Under the same setup as Sum-LoF, with DecidableEq ι, the equality holds: sum I M ((DirectSum.lof (AdicCompletion I R) ι (fun i ↦ AdicCompletion I (M i)) j) x) = map I (lof R ι M j) x for any j and x.
Русский
В той же постановке, как и Sum-LoF, с DecidableEq ι, выполняется тождество: sum I M ((DirectSum.lof (AdicCompletion I R) ι (fun i ↦ AdicCompletion I (M i)) j) x) = map I (lof R ι M j) x.
LaTeX
$$$ sum\, I\, M\, ((DirectSum.lof (AdicCompletion I R) ι (fun i \\mapsto AdicCompletion I (M i)) j)\\, x) = map I (lof R ι M j)\\, x $$$
Lean4
@[simp]
theorem sum_of [DecidableEq ι] (j : ι) (x : AdicCompletion I (M j)) :
sum I M ((DirectSum.of (fun i ↦ AdicCompletion I (M i)) j) x) = map I (lof R ι M j) x :=
by
rw [← lof_eq_of R]
apply sum_lof
