ofList_cons_smul — Mathlib

English

For any ideal I and linear map f, I · ⊤ ≤ comap f (I · ⊤).

Русский

Для любого идеала I и линейного отображения f выполняется I · ⊤ ≤ comap f (I · ⊤).

LaTeX

$$$I \\cdot \\top \\leq \\operatorname{comap} f (I \\cdot \\top)$$$

Lean4

theorem ofList_cons_smul {R} [CommSemiring R] (r : R) (rs : List R) {M} [AddCommMonoid M] [Module R M]
    (N : Submodule R M) : ofList (r :: rs) • N = r • N ⊔ ofList rs • N := by
  rw [ofList_cons, Submodule.sup_smul, Submodule.ideal_span_singleton_smul]

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