English
IsWeaklyRegular M (rs1 ++ rs2) iff IsWeaklyRegular M rs1 and IsWeaklyRegular (M ⧸ (Ideal.ofList rs1 • ⊤)) rs2.
Русский
IsWeaklyRegular M (rs1 ++ rs2) тогда и только тогда, когда IsWeaklyRegular M rs1 и IsWeaklyRegular на фактор-модуле rs2.
LaTeX
$$$IsWeaklyRegular(M, rs1 ++ rs2) \\iff IsWeaklyRegular(M, rs1) \\land IsWeaklyRegular\\left(M \\/ (Ideal.ofList(rs1) \\cdot \\top), rs2\\right)$$$
Lean4
theorem isWeaklyRegular_append_iff (rs₁ rs₂ : List R) :
IsWeaklyRegular M (rs₁ ++ rs₂) ↔
IsWeaklyRegular M rs₁ ∧ IsWeaklyRegular (M ⧸ (Ideal.ofList rs₁ • ⊤ : Submodule R M)) rs₂ :=
by
induction rs₁ generalizing M with
| nil =>
refine Iff.symm <| Iff.trans (and_iff_right (.nil R M)) ?_
refine (quotEquivOfEqBot _ ?_).isWeaklyRegular_congr rs₂
rw [Ideal.ofList_nil, bot_smul]
| cons r rs₁ ih =>
let e := quotOfListConsSMulTopEquivQuotSMulTopInner M r rs₁
rw [List.cons_append, isWeaklyRegular_cons_iff, isWeaklyRegular_cons_iff, ih, ← and_assoc, ←
e.isWeaklyRegular_congr rs₂]
