feat(LinearAlgebra): complements on spaces of dimension >1 or >n (#6348)

Mathlib/LinearAlgebra/Dimension.lean

@@ -1105,6 +1105,42 @@ theorem rank_eq_of_surjective (f : V →ₗ[K] V₁) (h : Surjective f) :
   rw [← rank_range_add_rank_ker f, ← rank_range_of_surjective f h]
 #align rank_eq_of_surjective rank_eq_of_surjective
 
+/-- Given a family of `n` linearly independent vectors in a space of dimension `> n`, one may extend
+the family by another vector while retaining linear independence. -/
+theorem exists_linear_independent_cons_of_lt_rank {n : ℕ} {v : Fin n → V}
+    (hv : LinearIndependent K v) (h : n < Module.rank K V) :
+    ∃ (x : V), LinearIndependent K (Fin.cons x v) := by
+  have A : Submodule.span K (range v) ≠ ⊤ := by
+    intro H
+    rw [← rank_top, ← H] at h
+    have : Module.rank K (Submodule.span K (range v)) ≤ n := by
+      have := Cardinal.mk_range_le_lift (f := v)
+      simp only [Cardinal.lift_id'] at this
+      exact (rank_span_le _).trans (this.trans (by simp))
+    exact lt_irrefl _ (h.trans_le this)
+  obtain ⟨x, hx⟩ : ∃ x, x ∉ Submodule.span K (range v) := by
+    contrapose! A
+    exact Iff.mpr Submodule.eq_top_iff' A
+  exact ⟨x, linearIndependent_fin_cons.2 ⟨hv, hx⟩⟩
+
+/-- Given a family of `n` linearly independent vectors in a space of dimension `> n`, one may extend
+the family by another vector while retaining linear independence. -/
+theorem exists_linear_independent_snoc_of_lt_rank {n : ℕ} {v : Fin n → V}
+    (hv : LinearIndependent K v) (h : n < Module.rank K V) :
+    ∃ (x : V), LinearIndependent K (Fin.snoc v x) := by
+  simpa [linearIndependent_fin_cons, ← linearIndependent_fin_snoc]
+    using exists_linear_independent_cons_of_lt_rank hv h
+
+/-- Given a nonzero vector in a space of dimension `> 1`, one may find another vector linearly
+independent of the first one. -/
+theorem exists_linear_independent_pair_of_one_lt_rank
+    (h : 1 < Module.rank K V) {x : V} (hx : x ≠ 0) :
+    ∃ y, LinearIndependent K ![x, y] := by
+  obtain ⟨y, hy⟩ := exists_linear_independent_snoc_of_lt_rank (linearIndependent_unique ![x] hx) h
+  have : Fin.snoc ![x] y = ![x, y] := Iff.mp List.ofFn_inj rfl
+  rw [this] at hy
+  exact ⟨y, hy⟩
+
 section
 
 variable [AddCommGroup V₂] [Module K V₂]

Mathlib/LinearAlgebra/FiniteDimensional.lean

@@ -1157,6 +1157,18 @@ theorem finrank_span_singleton {v : V} (hv : v ≠ 0) : finrank K (K ∙ v) = 1
     simp [hv]
 #align finrank_span_singleton finrank_span_singleton
 
+/-- In a one-dimensional space, any vector is a multiple of any nonzero vector -/
+lemma exists_smul_eq_of_finrank_eq_one
+    (h : finrank K V = 1) {x : V} (hx : x ≠ 0) (y : V) :
+    ∃ (c : K), c • x = y := by
+  have : Submodule.span K {x} = ⊤ := by
+    have : FiniteDimensional K V := finiteDimensional_of_finrank (zero_lt_one.trans_le h.symm.le)
+    apply eq_top_of_finrank_eq
+    rw [h]
+    exact finrank_span_singleton hx
+  have : y ∈ Submodule.span K {x} := by rw [this]; trivial
+  exact mem_span_singleton.1 this
+
 theorem Set.finrank_mono [FiniteDimensional K V] {s t : Set V} (h : s ⊆ t) :
     s.finrank K ≤ t.finrank K :=
   Submodule.finrank_mono (span_mono h)

Mathlib/LinearAlgebra/Finrank.lean

@@ -85,13 +85,16 @@ theorem finrank_lt_of_rank_lt {n : ℕ} (h : Module.rank K V < ↑n) : finrank K
   · exact nat_lt_aleph0 n
 #align finite_dimensional.finrank_lt_of_rank_lt FiniteDimensional.finrank_lt_of_rank_lt
 
-theorem rank_lt_of_finrank_lt {n : ℕ} (h : n < finrank K V) : ↑n < Module.rank K V := by
+theorem lt_rank_of_lt_finrank {n : ℕ} (h : n < finrank K V) : ↑n < Module.rank K V := by
   rwa [← Cardinal.toNat_lt_iff_lt_of_lt_aleph0, toNat_cast]
   · exact nat_lt_aleph0 n
   · contrapose! h
     rw [finrank, Cardinal.toNat_apply_of_aleph0_le h]
     exact n.zero_le
-#align finite_dimensional.rank_lt_of_finrank_lt FiniteDimensional.rank_lt_of_finrank_lt
+#align finite_dimensional.rank_lt_of_finrank_lt FiniteDimensional.lt_rank_of_lt_finrank
+
+theorem one_lt_rank_of_one_lt_finrank (h : 1 < finrank K V) : 1 < Module.rank K V := by
+  simpa using lt_rank_of_lt_finrank h
 
 theorem finrank_le_finrank_of_rank_le_rank
     (h : lift.{v'} (Module.rank K V) ≤ Cardinal.lift.{v} (Module.rank K V₂))
@@ -105,7 +108,7 @@ variable [Nontrivial K] [NoZeroSMulDivisors K V]
 
 /-- A finite dimensional space is nontrivial if it has positive `finrank`. -/
 theorem nontrivial_of_finrank_pos (h : 0 < finrank K V) : Nontrivial V :=
-  rank_pos_iff_nontrivial.mp (rank_lt_of_finrank_lt h)
+  rank_pos_iff_nontrivial.mp (lt_rank_of_lt_finrank h)
 #align finite_dimensional.nontrivial_of_finrank_pos FiniteDimensional.nontrivial_of_finrank_pos
 
 /-- A finite dimensional space is nontrivial if it has `finrank` equal to the successor of a
@@ -369,6 +372,27 @@ theorem span_lt_top_of_card_lt_finrank {s : Set V} [Fintype s]
   lt_top_of_finrank_lt_finrank (lt_of_le_of_lt (finrank_span_le_card _) card_lt)
 #align span_lt_top_of_card_lt_finrank span_lt_top_of_card_lt_finrank
 
+/-- Given a family of `n` linearly independent vectors in a finite-dimensional space of
+dimension `> n`, one may extend the family by another vector while retaining linear independence. -/
+theorem exists_linear_independent_snoc_of_lt_finrank {n : ℕ} {v : Fin n → V}
+    (hv : LinearIndependent K v) (h : n < finrank K V) :
+    ∃ (x : V), LinearIndependent K (Fin.snoc v x) :=
+  exists_linear_independent_snoc_of_lt_rank hv (lt_rank_of_lt_finrank h)
+
+/-- Given a family of `n` linearly independent vectors in a finite-dimensional space of
+dimension `> n`, one may extend the family by another vector while retaining linear independence. -/
+theorem exists_linear_independent_cons_of_lt_finrank {n : ℕ} {v : Fin n → V}
+    (hv : LinearIndependent K v) (h : n < finrank K V) :
+    ∃ (x : V), LinearIndependent K (Fin.cons x v) :=
+  exists_linear_independent_cons_of_lt_rank hv (lt_rank_of_lt_finrank h)
+
+/-- Given a nonzero vector in a finite-dimensional space of dimension `> 1`, one may find another
+vector linearly independent of the first one. -/
+theorem exists_linear_independent_pair_of_one_lt_finrank
+    (h : 1 < finrank K V) {x : V} (hx : x ≠ 0) :
+    ∃ y, LinearIndependent K ![x, y] :=
+  exists_linear_independent_pair_of_one_lt_rank (one_lt_rank_of_one_lt_finrank h) hx
+
 end DivisionRing
 
 end Span

Mathlib/LinearAlgebra/LinearIndependent.lean

@@ -187,6 +187,13 @@ theorem LinearIndependent.ne_zero [Nontrivial R] (i : ι) (hv : LinearIndependen
         · simp [h])
 #align linear_independent.ne_zero LinearIndependent.ne_zero
 
+lemma LinearIndependent.eq_zero_of_pair {x y : M} (h : LinearIndependent R ![x, y])
+    {s t : R} (h' : s • x + t • y = 0) : s = 0 ∧ t = 0 := by
+  have := linearIndependent_iff'.1 h Finset.univ ![s, t]
+  simp only [Fin.sum_univ_two, Matrix.cons_val_zero, Matrix.cons_val_one, Matrix.head_cons, h',
+    Finset.mem_univ, forall_true_left] at this
+  exact ⟨this 0, this 1⟩
+
 /-- A subfamily of a linearly independent family (i.e., a composition with an injective map) is a
 linearly independent family. -/
 theorem LinearIndependent.comp (h : LinearIndependent R v) (f : ι' → ι) (hf : Injective f) :
@@ -556,6 +563,14 @@ theorem LinearIndependent.units_smul {v : ι → M} (hv : LinearIndependent R v)
     rfl
 #align linear_independent.units_smul LinearIndependent.units_smul
 
+lemma LinearIndependent.eq_of_pair {x y : M} (h : LinearIndependent R ![x, y])
+    {s t s' t' : R} (h' : s • x + t • y = s' • x + t' • y) : s = s' ∧ t = t' := by
+  have : (s - s') • x + (t - t') • y = 0 := by
+    rw [← sub_eq_zero_of_eq h', ← sub_eq_zero]
+    simp only [sub_smul]
+    abel
+  simpa [sub_eq_zero] using h.eq_zero_of_pair this
+
 section Maximal
 
 universe v w