eq_zero_of_pair' — Mathlib

English

If x,y form a linearly independent pair, then equality s x = t y with x,y fixed implies s = 0 and t = 0 when the pair is LI.

Русский

Если x,y образуют линейно независимую пару, то равенство s x = t y с фиксированными x,y влечет s=0 и t=0 при LI-предположении.

LaTeX

$$$$\\forall x,y,\\; \\operatorname{LinearIndependent}_R(\\,[x,y]) \\Rightarrow (s x = t y \\Rightarrow s=0 \\land t=0).$$$$

Lean4

theorem eq_zero_of_pair' {x y : M} (h : LinearIndependent R ![x, y]) {s t : R} (h' : s • x = t • y) : s = 0 ∧ t = 0 :=
  by
  suffices H : s = 0 ∧ 0 = t from ⟨H.1, H.2.symm⟩
  exact h.eq_of_pair (by simpa using h')

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