smul_comap_le_comap_smul — Mathlib

English

Equality of threefold action: (I * J) • N = I • J • N.

Русский

Равенство тройного действия: (I J) • N = I • J • N.

LaTeX

$$$(I J) \\cdot N = I \\cdot J \\cdot N$$$

Lean4

@[simp]
theorem smul_comap_le_comap_smul (f : M →ₗ[R] M') (S : Submodule R M') (I : Ideal R) :
    I • S.comap f ≤ (I • S).comap f :=
  by
  refine Submodule.smul_le.mpr fun r hr x hx => ?_
  rw [Submodule.mem_comap] at hx ⊢
  rw [f.map_smul]
  exact Submodule.smul_mem_smul hr hx

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