isRegular_cons_iff — Mathlib

English

Regular M of a cons is equivalent to the conjoined regularity of its head and the regularity of its tail in the quotient.

Русский

Регулярность cons-структуры равна объединённой регулярности головы и регулярности хвоста в фактор-модуле.

LaTeX

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

Lean4

@[simp]
theorem isRegular_cons_iff (r : R) (rs : List R) :
    IsRegular M (r :: rs) ↔ IsSMulRegular M r ∧ IsRegular (QuotSMulTop r M) rs := by
  rw [isRegular_iff, isRegular_iff, isWeaklyRegular_cons_iff M r rs, ne_eq, top_eq_ofList_cons_smul_iff, and_assoc]

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