isRegular_cons_iff' — Mathlib

English

Variant of the cons decomposition that uses mapping through quotient of (Ideal.span { r }).

Русский

Вариант разложения через отображение по фактору по (Ideal.span { 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 isRegular_cons_iff' (r : R) (rs : List R) :
    IsRegular M (r :: rs) ↔
      IsSMulRegular M r ∧ IsRegular (QuotSMulTop r M) (rs.map (Ideal.Quotient.mk (Ideal.span { r }))) :=
  by
  conv => congr <;> rw [isRegular_iff, ne_eq]
  rw [isWeaklyRegular_cons_iff', ← restrictScalars_inj R (R ⧸ _), ← Ideal.map_ofList, ← Ideal.Quotient.algebraMap_eq,
    Ideal.smul_restrictScalars, restrictScalars_top, top_eq_ofList_cons_smul_iff, and_assoc]

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