Theorems · Definition · commutative algebra

AdicCompletion.ofTensorProductEquivOfPiFintype

{R : Type u_1} →
  [inst : CommRing R] →
    (I : Ideal R) →
      (ι : Type u_4) →
        [Fintype ι] →
          [DecidableEq ι] → TensorProduct R (AdicCompletion I R) (ι → R) ≃ₗ[AdicCompletion I R] AdicCompletion I (ι → R)

ofTensorProduct as an equiv in the case of M = R^ι where ι is finite.

Defined in

Mathlib.RingTheory.AdicCompletion.AsTensorProduct

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRingFintypeDecidableEq