isWeaklyRegular_append_iff' — Mathlib

English

A variant of append criterion with a different quotient-path.

Русский

Вариант условия добавления с другим путём просмотра через фактор-множество.

LaTeX

$$$IsWeaklyRegular(M, rs1 ++ rs2) \\iff IsWeaklyRegular M rs1 \\land IsWeaklyRegular(HasQuotient(M, rs1), rs2)$$$

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₂.map (Ideal.Quotient.mk (Ideal.ofList rs₁))) :=
  Iff.trans (isWeaklyRegular_append_iff M rs₁ rs₂) <|
    and_congr_right' <| Iff.symm <| isWeaklyRegular_map_algebraMap_iff (R ⧸ Ideal.ofList rs₁) _ rs₂

Похожие утверждения