top_eq_ofList_cons_smul_iff — Mathlib

English

The top submodule equality (⊤) with (r :: rs) smul is equivalent to the top equality with rs smul.

Русский

Равенство верхнего подмодуля при умножении на (r :: rs) эквивалентно верхнему равенству при rs.

LaTeX

$$$(\\top : Submodule R M) = \\text{Ideal.ofList} (r :: rs) \\cdot \\top \\;\\;\\;\\iff\\;\\;\\; (\\top : Submodule R (QuotSMulTop r M)) = \\text{Ideal.ofList rs} \\cdot \\top$$$

Lean4

theorem top_eq_ofList_cons_smul_iff :
    (⊤ : Submodule R M) = Ideal.ofList (r :: rs) • ⊤ ↔ (⊤ : Submodule R (QuotSMulTop r M)) = Ideal.ofList rs • ⊤ :=
  by
  conv => congr <;> rw [eq_comm, ← subsingleton_quotient_iff_eq_top]
  exact (quotOfListConsSMulTopEquivQuotSMulTopInner M r rs).toEquiv.subsingleton_congr

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