Theorems · Theorem · commutative algebra

RingTheory.Sequence.IsWeaklyRegular.prototype_perm

∀ {R : Type u_1} {M : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {rs : List R},
  RingTheory.Sequence.IsWeaklyRegular M rs →
    ∀ {rs' : List R},
      rs.Perm rs' →
        (∀ (a b : R) (rs' : List R),
            (a :: b :: rs').Subperm rs →
              have K := Submodule.torsionBy R (M ⧸ Ideal.ofList rs' • ⊤) b;
              K = a • K → K = ⊥) →
          RingTheory.Sequence.IsWeaklyRegular M rs'

Defined in

Mathlib.RingTheory.Regular.RegularSequence

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRingAddCommGroupModule