Theorems · Definition · commutative algebra

AdicCompletion.ofTensorProductEquivOfFiniteNoetherian

{R : Type u} →
  [inst : CommRing R] →
    (I : Ideal R) →
      (M : Type u) →
        [inst_1 : AddCommGroup M] →
          [inst_2 : Module R M] →
            [IsNoetherianRing R] →
              [Module.Finite R M] → TensorProduct R (AdicCompletion I R) M ≃ₗ[AdicCompletion I R] AdicCompletion I M

ofTensorProduct packaged as linear equiv if M is a finite R-module and R is Noetherian.

Defined in

Mathlib.RingTheory.AdicCompletion.AsTensorProduct

Cited by

6 results in Mathlib

Foundations

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

Assumes

CommRingAddCommGroupModuleIsNoetherianRingModule.Finite