of_forall_isTrivialRelation — Mathlib

English

If every relation ∑ f_i x_i = 0 in M is trivial, then M is flat over R.

Русский

Если каждая зависимость \sum_i f_i x_i = 0 в M тривиальна, тогда M плосок над R.

LaTeX

$$(∀ {l} {f : Fin l → R} {x : Fin l → M}, ∑ i, f i • x i = 0 → IsTrivialRelation f x) → Flat(R,M)$$

Lean4

/-- **Equational criterion for flatness**, backward direction.

If every relation $\sum_i f_i x_i = 0$ in $M$ is trivial, then $M$ is flat. -/
@[stacks 00HK]
theorem of_forall_isTrivialRelation
    (hfx : ∀ {l : ℕ} {f : Fin l → R} {x : Fin l → M}, ∑ i, f i • x i = 0 → IsTrivialRelation f x) : Flat R M :=
  iff_forall_isTrivialRelation.mpr hfx

Похожие утверждения