coe_truncLTLinearMap — Mathlib

English

The linear map truncLTLinearMap R c is exactly the truncation operator truncLT c, i.e., they are the same linear map.

Русский

Линейное отображение truncLTLinearMap R c совпадает с операцией усечения truncLT c; то есть это одно и то же линейное отображение.

LaTeX

$$$(truncLTLinearMap\\ R\\ c) = truncLT\\ c$$$

Lean4

@[simp]
theorem coe_truncLTLinearMap [DecidableLT Γ] (c : Γ) :
    (truncLTLinearMap R c : HahnSeries Γ V → HahnSeries Γ V) = truncLT c := by rfl

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