Theorems · Theorem · commutative algebra

RingTheory.Sequence.IsWeaklyRegular.cons

∀ {R : Type u_1} {M : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {r : R}
  {rs : List R},
  IsSMulRegular M r →
    RingTheory.Sequence.IsWeaklyRegular (QuotSMulTop r M) rs → RingTheory.Sequence.IsWeaklyRegular M (r :: rs)

Defined in

Mathlib.RingTheory.Regular.RegularSequence

Cited by

2 results in Mathlib

Foundations

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

Assumes

CommRingAddCommGroupModule