linearMap_toAddMonoidHom — Mathlib

English

The linear map mapRange with identity equals the identity linear map on the function space.

Русский

Линейное отображение mapRange с идентичностью равно тождественному отображению на пространстве функций.

LaTeX

$$$mapRange.linearMap\\; LinearMap.id = (LinearMap.id)$$$

Lean4

@[simp]
theorem linearMap_toAddMonoidHom (f : M →ₛₗ[σ₁₂] N) :
    (mapRange.linearMap f).toAddMonoidHom = (mapRange.addMonoidHom f.toAddMonoidHom : (α →₀ M) →+ _) :=
  AddMonoidHom.ext fun _ => rfl

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