R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ ∀ (x : TensorAlgebra R M), x ∈ LinearMap.range (ι R) → x ∈ 1 → x = 0
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ Disjoint (LinearMap.range (ι R)) 1
rw [Submodule.disjoint_def]
case intro.intro
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
r : R
hx : ↑(ι R) x = ↑(Algebra.linearMap R (TensorAlgebra R M)) r
⊢ ↑(Algebra.linearMap R (TensorAlgebra R M)) r = 0
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ ∀ (x : TensorAlgebra R M), x ∈ LinearMap.range (ι R) → x ∈ 1 → x = 0
rintro _ ⟨x, hx⟩ ⟨r, rfl⟩
case intro.intro
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
r : R
hx : x = 0 ∧ r = 0
⊢ ↑(Algebra.linearMap R (TensorAlgebra R M)) r = 0
case intro.intro
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
r : R
hx : ↑(ι R) x = ↑(Algebra.linearMap R (TensorAlgebra R M)) r
⊢ ↑(Algebra.linearMap R (TensorAlgebra R M)) r = 0
rw [Algebra.linearMap_apply, ι_eq_algebraMap_iff] at hx
no goals
case intro.intro
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
r : R
hx : x = 0 ∧ r = 0
⊢ ↑(Algebra.linearMap R (TensorAlgebra R M)) r = 0
rw [hx.2, map_zero]