map_pointwise_smul — Mathlib

English

For a linear map f, a submodule S of M', and an ideal I, we have I • S.comap f ≤ (I • S).comap f.

Русский

Для линейного отображения f, подподмодуля S ⊆ M' и идеала I выполняется: I • S.comap f ≤ (I • S).comap f.

LaTeX

$$$I \\cdot S^{\\mathrm{comap} f} \\le (I \\cdot S)^{\\mathrm{comap} f}$$$

Lean4

@[simp]
theorem map_pointwise_smul (r : R) (N : Submodule R M) (f : M →ₗ[R] M') : (r • N).map f = r • N.map f := by
  simp_rw [← ideal_span_singleton_smul, map_smul'']

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