no goals
R : Type ?u.13352
M : Type ?u.13355
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
m : M
⊢ ↑(TensorAlgebra.ι R) m ∈ LinearMap.range (TensorAlgebra.ι R) ^ 1
simpa only [pow_one] using LinearMap.mem_range_self _ m