linearEquiv_symm — Mathlib

English

Again, the image of mapRange.linearMap equals the comap of the coordinate-wise ranges via the canonical projection.

Русский

Образ mapRange.linearMap равен комапу по координатным образам через каноническую проекцию.

LaTeX

$$$\\mathrm{range}(\\mathrm{mapRange.linearMap}\\; f) = (\\mathrm{Submodule.pi}\\; \\mathrm{Set.univ}\\; (\\mathrm{LinearMap.range} \\; |\\!| f_i)).\\mathrm{comap}\\; (\\mathrm{coeFnLinearMap}\\; R)$$$

Lean4

@[simp]
theorem linearEquiv_symm (e : ∀ i, β₁ i ≃ₗ[R] β₂ i) :
    (mapRange.linearEquiv e).symm = mapRange.linearEquiv fun i => (e i).symm :=
  rfl

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