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 g : TensorAlgebra R M →ₐ[R] A
w : ↑(lift R).symm f = ↑(lift R).symm g
⊢ f = 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
f g : TensorAlgebra R M →ₐ[R] A
w : LinearMap.comp (AlgHom.toLinearMap f) (ι R) = LinearMap.comp (AlgHom.toLinearMap g) (ι R)
⊢ f = g
rw [← lift_symm_apply, ← lift_symm_apply] at w
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 g : TensorAlgebra R M →ₐ[R] A
w : ↑(lift R).symm f = ↑(lift R).symm g
⊢ f = g
exact (lift R).symm.injective w