linearEquiv_toLinearMap — Mathlib

English

The underlying linear map of mapRange.linearEquiv f is equal to the linear map induced by f.toLinearMap.

Русский

Базовое линейное отображение mapRange.linearEquiv f совпадает с линейным отображением, полученным из f.toLinearMap.

LaTeX

$$$$ (mapRange.linearEquiv f).toLinearMap = (mapRange.linearMap f.toLinearMap). $$$$

Lean4

@[simp]
theorem linearEquiv_toLinearMap (f : M ≃ₛₗ[σ₁₂] N) :
    (mapRange.linearEquiv f).toLinearMap = (mapRange.linearMap f.toLinearMap : (α →₀ M) →ₛₗ[σ₁₂] _) :=
  LinearMap.ext fun _ => rfl

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