pair_neg_left_iff — Mathlib

English

The independence of {[−x, y]} equals the independence of {[x, y]} via the pair_iff relation.

Русский

Независимость {[−x, y]} равна независимости {[x, y]} через отношение pair_iff.

LaTeX

$$$\\mathrm{LinearIndependent}_R(\\![ -x, y \\]) \\iff \\mathrm{LinearIndependent}_R(\\![ x, y \\])$$$

Lean4

@[simp]
theorem pair_neg_left_iff : LinearIndependent R ![-x, y] ↔ LinearIndependent R ![x, y] :=
  by
  rw [pair_iff, pair_iff]
  refine ⟨fun h s t hst ↦ ?_, fun h s t hst ↦ ?_⟩ <;> simpa using h (-s) t (by simpa using hst)

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