comap_smul — Mathlib

English

For a linear map f: V → V₂ and p ≤ V₂ a submodule, the preimage of p under a nonzero scalar multiple a•f coincides with the preimage under f.

Русский

Для линейного отображения f: V → V₂ и подмодуля p ⊆ V₂, предобраз p под отображением a·f (a ≠ 0) совпадает с предобразом p под f.

LaTeX

$$$ p.\\mathrm{comap} (a \\cdot f) = p.\\mathrm{comap} f $$$

Lean4

theorem comap_smul (f : V →ₗ[K] V₂) (p : Submodule K V₂) (a : K) (h : a ≠ 0) : p.comap (a • f) = p.comap f := by ext b;
  simp only [Submodule.mem_comap, p.smul_mem_iff h, LinearMap.smul_apply]

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