Theorems · Theorem · commutative algebra

Submodule.isPrimary_finsetInf

∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {ι : Type u_3}
  {s : Finset ι} {f : ι → Submodule R M} {i : ι},
  i ∈ s →
    (∀ ⦃y : ι⦄, y ∈ s → (f y).IsPrimary) →
      (∀ ⦃y : ι⦄, y ∈ s → ((f y).colon Set.univ).radical = ((f i).colon Set.univ).radical) → (s.inf f).IsPrimary

Defined in

Mathlib.RingTheory.IsPrimary

Cited by

2 results in Mathlib

Foundations

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

Assumes

CommSemiringAddCommMonoidModule