linearMap_id — Mathlib

English

For a finite X, the linear map corresponding to the identity on X is the identity on X → M.

Русский

Для конечного X линейное отображение, соответствующее тождественному отображению на X, является тождественным отображением на пространства функций X → M.

LaTeX

$$$\operatorname{linearMap} R\ M\ id = \mathrm{id}$$$

Lean4

@[simp]
theorem linearMap_id [Finite X] : linearMap R M (_root_.id : X → X) = .id := by classical aesop

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