English
If v is a linearly independent family, then the family of images under AlgHom.toLinearMap is also linearly independent.
Русский
Если v линейно независима, то образ под AlgHom.toLinearMap тоже линейно независим.
LaTeX
$$$\\mathrm{LinearIndependent}_L(\\mathrm{AlgHom.toLinearMap})$$$
Lean4
@[simp]
theorem pair_add_smul_add_smul_iff [Nontrivial R] :
LinearIndependent R ![a • x + b • y, c • x + d • y] ↔ LinearIndependent R ![x, y] ∧ a * d ≠ b * c :=
by
rcases eq_or_ne (a * d) (b * c) with h | h
· suffices ¬LinearIndependent R ![a • x + b • y, c • x + d • y] by simpa [h]
rw [pair_iff]
push_neg
by_cases hbd : b = 0 ∧ d = 0
· simp only [hbd.1, hbd.2, zero_smul, add_zero]
by_cases hac : a = 0 ∧ c = 0; · exact ⟨1, 0, by simp [hac.1, hac.2], by simp⟩
refine ⟨c • 1, -a • 1, ?_, by aesop⟩
simp only [smul_assoc, one_smul, neg_smul]
module
refine ⟨d • 1, -b • 1, ?_, by contrapose! hbd; simp_all⟩
simp only [smul_add, smul_assoc, one_smul, smul_smul, mul_comm d, h]
module
refine ⟨fun h' ↦ ⟨?_, h⟩, fun ⟨h₁, h₂⟩ ↦ pair_add_smul_add_smul_iff_aux _ _ _ _ h₂ h₁⟩
suffices LinearIndependent R ![(a * d - b * c) • x, (a * d - b * c) • y] by
rwa [pair_smul_iff (sub_ne_zero_of_ne h)] at this
convert pair_add_smul_add_smul_iff_aux d (-b) (-c) a (by simpa [mul_comm d a]) h' using 1
ext i; fin_cases i <;> simp <;> module
