map_smul' — Mathlib

English

For a linear map f: V → V₂, a submodule p ≤ V and a ∈ K, p.map (a•f) equals the supremum over all nonzero scalars of p.map f.

Русский

Для линейного отображения f: V → V₂, подмодуля p ⊆ V и скаляра a ≠ 0, p.map (a•f) равняется наибольшей верхней границе (супремуму) изображений p.map f по ненулевым скалярам.

LaTeX

$$$ p.map (a \\cdot f) = \\bigvee_{t \\neq 0} p.map f $$$

Lean4

theorem map_smul' (f : V →ₗ[K] V₂) (p : Submodule K V) (a : K) : p.map (a • f) = ⨆ _ : a ≠ 0, map f p := by
  classical by_cases h : a = 0 <;> simp [h, Submodule.map_smul]

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