pair_iffₛ — Mathlib

English

A two-element ordered family [x, y] is linearly independent iff the only scalars s,t giving s x + t y = s' x + t' y are s = s' and t = t'.

Русский

Порядковая пара {x,y} линейно независима тогда, когда единственные коэффициенты s,t и s',t' удовлетворяющие s x + t y = s' x + t' y являются s=s' и t=t'.

LaTeX

$$$$\\operatorname{LinearIndependent}_R\\big([x,y]\\big) \\iff \\forall s,t,s',t'\\in R,\\; s x + t y = s' x + t' y \\Rightarrow (s=s' \\land t=t').$$$$

Lean4

theorem pair_iffₛ {x y : M} :
    LinearIndependent R ![x, y] ↔ ∀ (s t s' t' : R), s • x + t • y = s' • x + t' • y → s = s' ∧ t = t' := by
  simp [Fintype.linearIndependent_iffₛ, Fin.forall_fin_two, ← FinVec.forall_iff]; rfl

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