pair_iff' — Mathlib

English

Over a division ring K, LinearIndependent K ![x,y] is equivalent to: for all a in K, a x ≠ y, provided x ≠ 0.

Русский

Пусть K — деление кольцо. Тогда LinearIndependent K ![x,y] эквивалентно: для всех a ∈ K выполняется a x ≠ y при условии x ≠ 0.

LaTeX

$$$x \neq 0 \Rightarrow \text{LinearIndependent}_K(\,[x,y]\!) \iff \forall a \in K, a \cdot x \neq y$$$

Lean4

/-- Also see `LinearIndependent.pair_iff` for the version over arbitrary rings. -/
theorem pair_iff' {x y : V} (hx : x ≠ 0) : LinearIndependent K ![x, y] ↔ ∀ a : K, a • x ≠ y :=
  by
  rw [← linearIndepOn_univ, ← Finset.coe_univ, show @Finset.univ (Fin 2) _ = {0, 1} from rfl, Finset.coe_insert,
    Finset.coe_singleton, linearIndepOn_pair_iff _ (by simp) (by simpa)]
  simp

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