English
The sequence r :: rs is weakly regular on M iff r is regular on M and rs is weakly regular on the quotient M ⧸ rM.
Русский
Последовательность r :: rs является слабой регулярной на M тогда и только тогда, когда r регулярен на M и rs является слабой регулярной на фактор-модуле M / rM.
LaTeX
$$$IsWeaklyRegular(M, r :: rs) \\iff IsSMulRegular(M, r) \\land IsWeaklyRegular(QuotSMulTop r M, rs)$$$
Lean4
@[simp]
theorem isWeaklyRegular_cons_iff (r : R) (rs : List R) :
IsWeaklyRegular M (r :: rs) ↔ IsSMulRegular M r ∧ IsWeaklyRegular (QuotSMulTop r M) rs :=
have := Eq.trans (congrArg (· • ⊤) Ideal.ofList_nil) (bot_smul ⊤)
let e i := quotOfListConsSMulTopEquivQuotSMulTopInner M r (rs.take i)
Iff.trans (isWeaklyRegular_iff_Fin _ _) <|
Iff.trans Fin.forall_iff_succ <|
and_congr ((quotEquivOfEqBot _ this).isSMulRegular_congr r) <|
Iff.trans (forall_congr' fun i => (e i).isSMulRegular_congr (rs.get i)) (isWeaklyRegular_iff_Fin _ _).symm
