Theorems · Inductive type · commutative algebra

RingTheory.Sequence.IsWeaklyRegular

{R : Type u_1} → (M : Type u_3) → [inst : CommRing R] → [inst_1 : AddCommGroup M] → [Module R M] → List R → Prop

A sequence [r₁, …, rₙ] is weakly regular on M iff rᵢ is regular on M⧸(r₁, …, rᵢ₋₁)M for all 1 ≤ i ≤ n.

Defined in

Mathlib.RingTheory.Regular.RegularSequence

Cited by

40 results in Mathlib

Foundations

Depth 6 from the axioms · uses no axioms

Assumes

CommRingAddCommGroupModule