isWeaklyRegular_cons_iff' — Mathlib

English

The regularity of a list r :: rs is equivalent to the regularity of r together with the regularity of rs mapped through the quotient by r, i.e. rs mapped by quotient map of (Ideal span {r}).

Русский

Регулярность списка r :: rs эквивалентна регулярности элемента 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 isWeaklyRegular_cons_iff' (r : R) (rs : List R) :
    IsWeaklyRegular M (r :: rs) ↔
      IsSMulRegular M r ∧ IsWeaklyRegular (QuotSMulTop r M) (rs.map (Ideal.Quotient.mk (Ideal.span { r }))) :=
  Iff.trans (isWeaklyRegular_cons_iff M r rs) <|
    and_congr_right' <| Iff.symm <| isWeaklyRegular_map_algebraMap_iff (R ⧸ Ideal.span { r }) _ rs

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