Range of LinearMap.prod

Stream: Is there code for X?

[Michael Rothgang]

Do we really not have this?

import Mathlib

open Function Set

variable {𝕜 : Type*} [NontriviallyNormedField 𝕜] {E E' F F' G : Type*}
  [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E']
  [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedAddCommGroup F'] [NormedSpace 𝕜 F']

namespace LinearMap

lemma range_prodMap {f : E →L[𝕜] F} {g : E' →L[𝕜] F'} :
    range (f.prodMap g) = (range f).prod (range g) := by
  ext x
  rw [Submodule.mem_prod]
  simp_rw [LinearMap.mem_range]
  constructor <;> intro h
  · have : x ∈ Set.range (Prod.map f g) := h
    rcases h with ⟨⟨y1, y₂⟩, hy⟩
    all_goals simp_all
  · choose y₁ hy₁ using h.1
    choose y₂ hy₂ using h.2
    use (y₁, y₂), by simp [hy₁, hy₂]

[Michael Rothgang]

@loogle LinearMap, "range", "prod"

[Michael Rothgang]

None of these mentions Prod.map.

[Junyan Xu]

lemma range_prodMap {f : E →L[𝕜] F} {g : E' →L[𝕜] F'} :
    range (f.prodMap g) = (range f).prod (range g) := by
  ext; simp [Prod.ext_iff]

works