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
f : M →ₗ[R] A
g : TensorAlgebra R M →ₐ[R] A
⊢ LinearMap.comp (AlgHom.toLinearMap g) (ι R) = f ↔ ↑(lift R).symm g = f
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
f : M →ₗ[R] A
g : TensorAlgebra R M →ₐ[R] A
⊢ LinearMap.comp (AlgHom.toLinearMap g) (ι R) = f ↔ g = ↑(lift R) f
rw [← (lift R).symm_apply_eq]
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
f : M →ₗ[R] A
g : TensorAlgebra R M →ₐ[R] A
⊢ LinearMap.comp (AlgHom.toLinearMap g) (ι R) = f ↔ ↑(lift R).symm g = f
simp only [lift, Equiv.coe_fn_symm_mk]