English
If the expression sum_i m_i ⊗ n_i vanishes trivially, then the total sum equals zero in the tensor product: ∑_i m_i ⊗ n_i = 0 whenever VanishesTrivially R m n.
Русский
Если выражение ∑_i m_i ⊗ n_i исчезает тривиально, тогда сумма в тензорном произведении равна нулю: ∑_i m_i ⊗ n_i = 0, если VanishesTrivially R m n.
LaTeX
$$$ \\text{VanishesTrivially}_R(m, n) \\;\Longrightarrow\; \\sum_{i} m_i \\otimes n_i = 0$$$
Lean4
/-- **Equational criterion for vanishing**
[A. Altman and S. Kleiman, *A term of commutative algebra* (Lemma 8.16)][altman2021term],
backward direction.
If the expression $\sum_i m_i \otimes n_i$ vanishes trivially, then it vanishes.
That is, $\sum_i m_i \otimes n_i = 0$. -/
theorem sum_tmul_eq_zero_of_vanishesTrivially (hmn : VanishesTrivially R m n) : ∑ i, m i ⊗ₜ n i = (0 : M ⊗[R] N) :=
by
obtain ⟨k, a, y, h₁, h₂⟩ := hmn
simp_rw [h₁, tmul_sum, tmul_smul]
rw [Finset.sum_comm]
simp_rw [← tmul_smul, ← smul_tmul, ← sum_tmul, h₂, zero_tmul, Finset.sum_const_zero]
