English
If there exist κ finite and appropriate a and y satisfying linear relations making n_i as sums of a_{i j} y_j and sums of a_{i j} m_i vanish for all j, then the tensor expression vanishes trivially as defined in the vanishing criterion.
Русский
Если существует конечный κ и соответствующие a и y, удовлетворяющие линейным условиям, так что n_i выражаются как суммы a_{i j} y_j, а суммы a_{i j} m_i по j обращаются в ноль, тогда выражение в тензорном произведении исчезает тривиально.
LaTeX
$$$$\\exists κ\\,[Fintype\\ κ]\\ (a:ι→κ→R)\; (y:κ→N),\\; (\\forall i, n_i=\\sum_j a_{i j}y_j) \\land (\\forall j, \\sum_i a_{i j} m_i = 0) \\Rightarrow \\mathrm{VanishesTrivially}\\ R\\ m\\ n.$$$$
Lean4
/-- An expression $\sum_i m_i \otimes n_i$ in $M \otimes N$
*vanishes trivially* if there exist a finite index type $\kappa$ = `Fin k`,
elements $(y_j)_{j \in \kappa}$ of $N$, and elements $(a_{ij})_{i \in \iota, j \in \kappa}$ of $R$
such that for all $i$,
$$n_i = \sum_j a_{ij} y_j$$
and for all $j$,
$$\sum_i a_{ij} m_i = 0.$$
Note that this condition is not symmetric in $M$ and $N$.
(The terminology "trivial" comes from [Stacks 00HK](https://stacks.math.columbia.edu/tag/00HK).) -/
abbrev VanishesTrivially : Prop :=
∃ (k : ℕ) (a : ι → Fin k → R) (y : Fin k → N), (∀ i, n i = ∑ j, a i j • y j) ∧ ∀ j, ∑ i, a i j • m i = 0
