cons — Mathlib

English

Regular M (r :: rs) is equivalent to the conjunction of regularity of r and regularity on the quotient with rs mapped accordingly.

Русский

Регулярность M (r :: rs) эквивалентна сочетанию регулярности r и регулярности на фактор-модуле.

LaTeX

$$$IsRegular(M, r :: rs) \\iff IsSMulRegular(M, r) \\land IsRegular(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 : IsRegular (QuotSMulTop r M) rs) :
    IsRegular M (r :: rs) :=
  (isRegular_cons_iff M r rs).mpr ⟨h1, h2⟩

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