Theorems · Theorem · commutative algebra

AdicCompletion.sum_lof

∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) {ι : Type u_6} (M : ι → Type u_7)
  [inst_1 : (i : ι) → AddCommGroup (M i)] [inst_2 : (i : ι) → Module R (M i)] [inst_3 : DecidableEq ι] (j : ι)
  (x : AdicCompletion I (M j)),
  (AdicCompletion.sum I M) ((DirectSum.lof (AdicCompletion I R) ι (fun i => AdicCompletion I (M i)) j) x) =
    (AdicCompletion.map I (DirectSum.lof R ι M j)) x

Defined in

Mathlib.RingTheory.AdicCompletion.Functoriality

Cited by

2 results in Mathlib

Foundations

Depth 110 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingAddCommGroupModuleDecidableEq