Theorems · Definition · commutative algebra
Submodule.IsPrimary
{R : Type u_1} →
{M : Type u_2} → [inst : CommSemiring R] → [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → Submodule R M → PropA proper submodule S : Submodule R M is primary iff
r • x ∈ S implies x ∈ S or ∃ n : ℕ, r ^ n • (⊤ : Submodule R M) ≤ S.
This generalizes Ideal.IsPrimary.
- Defined in
- Mathlib.RingTheory.IsPrimary
- Cited by
- 16 results in Mathlib
- Foundations
- Depth 68 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Modulestatement and proof · cited by 20,661
- AddCommMonoidstatement and proof · cited by 12,281
- CommSemiringstatement and proof · cited by 10,911
- Top.topproof · cited by 9,680
- Submodulestatement and proof · cited by 7,192
Cited by20
Results whose statement or proof uses this declaration.
- Ideal.IsPrimaryproof · cited by 13
- IsLaskerproof · cited by 5
- Submodule.IsMinimalPrimaryDecomposition.primarystatement · cited by 3
- Submodule.IsPrimary.infstatement and proof · cited by 2
- Submodule.IsPrimary.isPrime_radical_colonstatement and proof · cited by 2
- Submodule.IsPrimary.mem_or_memstatement and proof · cited by 2
- Submodule.isPrimary_decomposition_pairwise_ne_radicalstatement and proof · cited by 2
- Submodule.isPrimary_finsetInfstatement and proof · cited by 2
- Submodule.IsLasker.exists_isMinimalPrimaryDecompositionproof · cited by 2
- Submodule.exists_minimal_isPrimary_decomposition_of_isPrimary_decompositionstatement and proof · cited by 2
- Submodule.IsPrimary.radical_colon_singleton_eq_itestatement and proof · cited by 1
- Submodule.IsPrimary.radical_colon_singleton_of_notMemstatement and proof · cited by 1