lmapDomain_comp — Mathlib

English

The lmapDomain map with the identity is the identity map on Finsupp: lmapDomain M R id = LinearMap.id.

Русский

Координатное отображение с идентичностью равно тождественному отображению: lmapDomain M R id = LinearMap.id.

LaTeX

$$$(lmapDomain M R id) = LinearMap.id$$$

Lean4

theorem lmapDomain_comp (f : α → α') (g : α' → α'') :
    lmapDomain M R (g ∘ f) = (lmapDomain M R g).comp (lmapDomain M R f) :=
  LinearMap.ext fun _ => mapDomain_comp

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