Theorems · Definition · commutative algebra

Submodule.IsAssociatedPrime.casesOn

{R : Type u_1} →
  {M : Type u_2} →
    [inst : CommSemiring R] →
      [inst_1 : AddCommMonoid M] →
        [inst_2 : Module R M] →
          {N : Submodule R M} →
            {I : Ideal R} →
              {motive : N.IsAssociatedPrime I → Sort u} →
                (t : N.IsAssociatedPrime I) →
                  ((toIsPrime : I.IsPrime) → (eq_radical_colon : ∃ x, I = (N.colon {x}).radical) → motive ⋯) → motive t

Defined in

Mathlib.RingTheory.Ideal.AssociatedPrime.Basic

Cited by

8 results in Mathlib

Foundations

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

Assumes

CommSemiringAddCommMonoidModule