cons' — Mathlib

English

Variant of the cons criterion with a quotient-map modification.

Русский

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

LaTeX

$$$IsWeaklyRegular(M, r :: rs) \\iff IsSMulRegular(M, r) \\land IsWeaklyRegular(QuotSMulTop r M, rs.map (Ideal.Quotient.mk (Ideal.span { r }))) rs$$$

Lean4

theorem cons' {r : R} {rs : List R} (h1 : IsSMulRegular M r)
    (h2 : IsWeaklyRegular (QuotSMulTop r M) (rs.map (Ideal.Quotient.mk (Ideal.span { r })))) :
    IsWeaklyRegular M (r :: rs) :=
  (isWeaklyRegular_cons_iff' M r rs).mpr ⟨h1, h2⟩

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