cons — Mathlib

English

IsWeaklyRegular M (rs1++rs2) is equivalent to IsWeaklyRegular M rs1 and IsWeaklyRegular (M / (Ideal.ofList rs1 • ⊤)) rs2.

Русский

Слабая регулярность M (rs1 ++ rs2) эквивалентна IsWeaklyRegular M rs1 и IsWeaklyRegular (M /(I(rs1) • ⊤)) rs2.

LaTeX

$$$IsWeaklyRegular(M, rs1++rs2) \\iff IsWeaklyRegular(M, rs1) \\land IsWeaklyRegular\\left(M \\/ (Ideal.ofList(rs1) \\cdot \\top), rs2\\right)$$$

Lean4

theorem cons {r : R} {rs : List R} (h1 : IsSMulRegular M r) (h2 : IsWeaklyRegular (QuotSMulTop r M) rs) :
    IsWeaklyRegular M (r :: rs) :=
  (isWeaklyRegular_cons_iff M r rs).mpr ⟨h1, h2⟩

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