Theorems · Definition · commutative algebra

RingTheory.Sequence.IsWeaklyRegular.recIterModByRegular

{R : Type u_1} →
  [inst : CommRing R] →
    {motive :
        (M : Type v) →
          [inst_1 : AddCommGroup M] →
            [inst_2 : Module R M] → (rs : List R) → RingTheory.Sequence.IsWeaklyRegular M rs → Sort u_7} →
      ((M : Type v) → [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → motive M [] ⋯) →
        ({M : Type v} →
            [inst_1 : AddCommGroup M] →
              [inst_2 : Module R M] →
                (r : R) →
                  (rs : List R) →
                    (h1 : IsSMulRegular M r) →
                      (h2 : RingTheory.Sequence.IsWeaklyRegular (QuotSMulTop r M) rs) →
                        motive (QuotSMulTop r M) rs h2 → motive M (r :: rs) ⋯) →
          {M : Type v} →
            [inst_1 : AddCommGroup M] →
              [inst_2 : Module R M] → {rs : List R} → (h : RingTheory.Sequence.IsWeaklyRegular M rs) → motive M rs h

Weakly regular sequences can be inductively characterized by: * The empty sequence is weakly regular on any module. * If r is regular on M and rs is a weakly regular sequence on M⧸rM then the sequence obtained from rs by prepending r is weakly regular on M. This is the induction principle produced by the inductive definition above. The motive will usually be valued in Prop, but Sort* works too.

Defined in

Mathlib.RingTheory.Regular.RegularSequence

Cited by

3 results in Mathlib

Foundations

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

Assumes

CommRingAddCommGroupModule