cons' — Mathlib

English

If r is regular on M and rs is regular on the quotient, then r :: rs is regular on M.

Русский

Если r регулярна на M и rs регулярно на факторте, то r :: rs регулярна на M.

LaTeX

$$$IsRegular(M, r :: rs) \\iff IsSMulRegular(M, r) \\land IsRegular(QuotSMulTop r M, rs)$$$

Lean4

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

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