Theorems · Definition · commutative algebra

Ideal.primaryComponent

{A : Type u_1} →
  (M : Type u_2) → [inst : CommRing A] → Ideal A → [inst_1 : AddCommMonoid M] → [inst_2 : Module A M] → Submodule A M

The I-primaryComponent component of a module M where I is an ideal of A.

Defined in

Mathlib.Algebra.Module.Torsion.PrimaryComponent

Cited by

10 results in Mathlib

Foundations

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

Assumes

CommRingAddCommMonoidModule