ι_comp_lift — Mathlib

English

The lift map is compatible with composing with ι: lifting the composition g ∘ ι equals g itself; i.e., lift R (g ∘ ι) = g.

Русский

Лифтинг совместим с композициями: подъем g ∘ ι равен g.

LaTeX

$$lift R (g.toLinearMap.comp (ι R)) = g$$

Lean4

@[simp]
theorem ι_comp_lift {A : Type*} [Semiring A] [Algebra R A] (f : M →ₗ[R] A) : (lift R f).toLinearMap.comp (ι R) = f := by
  convert (lift R).symm_apply_apply f

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