map_smul — Mathlib

English

For nonzero a, the image of a submodule p under a•f is the same as the image under f.

Русский

Для ненулевого скаляра a и подмодуля p образ p под a·f совпадает с образом p под f.

LaTeX

$$$ p.map (a \\cdot f) = p.map f $$$

Lean4

protected theorem map_smul (f : V →ₗ[K] V₂) (p : Submodule K V) (a : K) (h : a ≠ 0) : p.map (a • f) = p.map f :=
  le_antisymm (by rw [map_le_iff_le_comap, comap_smul f _ a h, ← map_le_iff_le_comap])
    (by rw [map_le_iff_le_comap, ← comap_smul f _ a h, ← map_le_iff_le_comap])

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