Theorems · Inductive type · commutative algebra

Ideal.Filtration

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

An I-filtration on the module M is a sequence of decreasing submodules N i such that I • (N i) ≤ N (i + 1). Note that we do not require the filtration to start from ⊤.

Defined in

Mathlib.RingTheory.Filtration

Cited by

32 results in Mathlib

Foundations

Depth 15 from the axioms · uses no axioms

Assumes

CommRingAddCommGroupModule