map_le_smul_top — Mathlib

English

For a linear map f : R → M and an ideal I, the image of I under f is contained in I · ⊤_M.

Русский

Для линейного отображения f: R → M и идеала I образ I под действием f лежит внутри I · ⊤_M.

LaTeX

$$$\\mathrm{Submodule.map}\, f\, I \\le I \\cdot (\\top : Submodule R M)$$$

Lean4

theorem map_le_smul_top (I : Ideal R) (f : R →ₗ[R] M) : Submodule.map f I ≤ I • (⊤ : Submodule R M) :=
  by
  rintro _ ⟨y, hy, rfl⟩
  rw [← mul_one y, ← smul_eq_mul, f.map_smul]
  exact smul_mem_smul hy mem_top

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