Theorems · Definition · commutative algebra

AdicCompletion

{R : Type u_1} → [inst : CommRing R] → Ideal R → (M : Type u_4) → [inst_1 : AddCommGroup M] → [Module R M] → Type u_4

The completion of a module with respect to an ideal. This is Hausdorff but not necessarily complete: a classical sufficient condition for completeness is that I be finitely generated [Stacks, 05GG].

Defined in

Mathlib.RingTheory.AdicCompletion.Basic

Cited by

160 results in Mathlib

Foundations

Depth 91 from the axioms, rests on 1,496 definitions · uses propext, Classical.choice, Quot.sound

Assumes

CommRingAddCommGroupModule