English
If a finite matrix has a left inverse, then the corresponding family is affinely independent.
Русский
Если для матрицы конечного размера существует левый обратный, соответствующее семейство аффинно независимо.
LaTeX
$$$\\exists A: \\text{Matrix}_{\\iota \\times \\iota'}(k),\\ b.toMatrix p \\cdot A = 1 \\Rightarrow \\operatorname{AffineIndependent}_k(p).$$$
Lean4
/-- Given a family of points `p : ι' → P` and an affine basis `b`, if the matrix whose rows are the
coordinates of `p` with respect `b` has a right inverse, then `p` is affine independent. -/
theorem affineIndependent_of_toMatrix_right_inv [Fintype ι] [Finite ι'] [DecidableEq ι'] (p : ι' → P)
{A : Matrix ι ι' k} (hA : b.toMatrix p * A = 1) : AffineIndependent k p :=
by
cases nonempty_fintype ι'
rw [affineIndependent_iff_eq_of_fintype_affineCombination_eq]
intro w₁ w₂ hw₁ hw₂ hweq
have hweq' : w₁ ᵥ* b.toMatrix p = w₂ ᵥ* b.toMatrix p := by
ext j
change (∑ i, w₁ i • b.coord j (p i)) = ∑ i, w₂ i • b.coord j (p i)
rw [← Finset.univ.affineCombination_eq_linear_combination _ _ hw₁, ←
Finset.univ.affineCombination_eq_linear_combination _ _ hw₂, ← Function.comp_def (b.coord j) p, ←
Finset.univ.map_affineCombination p w₁ hw₁, ← Finset.univ.map_affineCombination p w₂ hw₂, hweq]
replace hweq' := congr_arg (fun w => w ᵥ* A) hweq'
simpa only [Matrix.vecMul_vecMul, hA, Matrix.vecMul_one] using hweq'
