English
Let R be a commutative ring and M an R-module. For a list rs of ring elements, the sequence rs is weakly regular on M exactly when, for every index i in the finite index set {0,...,length(rs)-1}, the element rs[i] is regular on the quotient M modulo the submodule generated by the first i elements of rs.
Русский
Пусть R — коммутативное кольцо, M — R-модуль. Для списка rs элементов кольца последовательность rs является слабой регулярной на M тогда и только тогда, когда для каждого индекса i из {0, ..., length(rs)-1} элемент rs[i] является регулярным на фактор-модуле M / ((порожденная) подпростольство, порожденное начальными i элементами rs).
LaTeX
$$$IsWeaklyRegular(M, rs) \\iff \\forall i : \\Fin(\\text{rs.length}), \\, IsSMulRegular\\left(M \\big/ \\big(\\mathrm{ofList}(\\mathrm{rs.take}(i)) \\;\\cdot\\; \\top\\big), \\ rs[i]\\right)$$$
Lean4
theorem isWeaklyRegular_iff_Fin (rs : List R) :
IsWeaklyRegular M rs ↔ ∀ (i : Fin rs.length), IsSMulRegular (M ⧸ (ofList (rs.take i) • ⊤ : Submodule R M)) rs[i] :=
Iff.trans (isWeaklyRegular_iff M rs) (Iff.symm Fin.forall_iff)
