comap_smul' — Mathlib

English

For a linear map f: V → V₂, p ≤ V₂ and a ∈ K, the equality p.comap (a • f) = ⨅_{a ≠ 0} p.comap f holds.

Русский

Для линейного отображения f: V → V₂, p ≤ V₂ и a ≠ 0 выполняется p.comap (a • f) = ⨅_{a ≠ 0} p.comap f.

LaTeX

$$$ p.\\mathrm{comap} (a \\cdot f) = \\bigwedge_{t \\neq 0} p.\\mathrm{comap} f $$$

Lean4

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

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