R : Type u_2
inst✝⁴ : CommSemiring R
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_1
inst✝¹ : Semiring A
inst✝ : Algebra R A
g : TensorAlgebra R M →ₐ[R] A
⊢ ↑(lift R) (↑(lift R).symm g) = g
R : Type u_2
inst✝⁴ : CommSemiring R
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_1
inst✝¹ : Semiring A
inst✝ : Algebra R A
g : TensorAlgebra R M →ₐ[R] A
⊢ ↑(lift R) (LinearMap.comp (AlgHom.toLinearMap g) (ι R)) = g
rw [← lift_symm_apply]
no goals
R : Type u_2
inst✝⁴ : CommSemiring R
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_1
inst✝¹ : Semiring A
inst✝ : Algebra R A
g : TensorAlgebra R M →ₐ[R] A
⊢ ↑(lift R) (↑(lift R).symm g) = g
exact (lift R).apply_symm_apply g