English
If M is flat, then every relation ∑ i f_i x_i = 0 in M with coefficients f_i ∈ R and elements x_i ∈ M is a trivial relation.
Русский
Если M плосок, то каждая зависимость вида \sum_i f_i x_i = 0 с коэффициентами f_i в R и элементами x_i в M тривиальна.
LaTeX
$$$Flat(R,M) \Rightarrow \forall \{l\}, f: \{1,\dots,l\} \to R, x: \{1,\dots,l\} \to M, \; \sum_{i=1}^l f(i)\,x(i)=0 \Rightarrow \text{IsTrivialRelation}(f,x)$$$
Lean4
/-- **Equational criterion for flatness**, forward direction.
If $M$ is flat, then every relation $\sum_i f_i x_i = 0$ in $M$ is trivial. -/
@[stacks 00HK]
theorem isTrivialRelation_of_sum_smul_eq_zero [Flat R M] {ι : Type*} [Fintype ι] {f : ι → R} {x : ι → M}
(h : ∑ i, f i • x i = 0) : IsTrivialRelation f x :=
(Fintype.equivFin ι).symm.isTrivialRelation_comp.mp <|
iff_forall_isTrivialRelation.mp ‹_› <| by simpa only [← (Fintype.equivFin ι).symm.sum_comp] using h
