English
If hs and ht are linear independence of elements in s and t respectively, then the combined embedding into the disjoint union is independent.
Русский
Если hs и ht линейно независимы на s и t, то их объединение через inl/inr в плоское произведение сохраняет независимость.
LaTeX
$$$\\mathrm{LinearIndependent}_R(\\text{Sum.Inl/Inr map})$$$
Lean4
theorem pair_smul_iff {u : S} (hu : u ≠ 0) : LinearIndependent R ![u • x, u • y] ↔ LinearIndependent R ![x, y] :=
by
simp only [LinearIndependent.pair_iff]
refine ⟨fun h s t hst ↦ ?_, fun h s t hst ↦ ?_⟩
· exact h s t (by rw [← smul_comm u s, ← smul_comm u t, ← smul_add, hst, smul_zero])
· specialize h (u • s) (u • t) (by rw [smul_assoc, smul_assoc, smul_comm u s, smul_comm u t, hst])
exact ⟨(smul_eq_zero_iff_right hu).mp h.1, (smul_eq_zero_iff_right hu).mp h.2⟩
