Theorems · Definition · commutative algebra

AdicCompletion.ofTensorProduct

{R : Type u_1} →
  [inst : CommRing R] →
    (I : Ideal R) →
      (M : Type u_2) →
        [inst_1 : AddCommGroup M] →
          [inst_2 : Module R M] → TensorProduct R (AdicCompletion I R) M →ₗ[AdicCompletion I R] AdicCompletion I M

The natural AdicCompletion I R-linear map from AdicCompletion I R ⊗[R] M to the adic completion of M.

Defined in

Mathlib.RingTheory.AdicCompletion.AsTensorProduct

Cited by

10 results in Mathlib

Foundations

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

Assumes

CommRingAddCommGroupModule