feat: add an element to a linear indep family, more general version (#31515)

Author: YaelDillies

Mathlib/Analysis/Normed/Unbundled/FiniteExtension.lean

@@ -181,8 +181,7 @@ theorem exists_nonarchimedean_pow_mul_seminorm_of_finiteDimensional (hfd : Finit
     ∃ f : AlgebraNorm K L, IsPowMul f ∧ (∀ (x : K), f ((algebraMap K L) x) = ‖x‖) ∧
       IsNonarchimedean f := by
   -- Choose a basis B = {1, e2,..., en} of the K-vector space L
-  set h1 : LinearIndepOn K id ({1} : Set L) :=
-    LinearIndepOn.id_singleton _ one_ne_zero
+  have h1 : LinearIndepOn K id ({1} : Set L) := .singleton one_ne_zero
   set ι := { x // x ∈ LinearIndepOn.extend h1 (Set.subset_univ ({1} : Set L)) }
   set B : Basis ι K L := Basis.extend h1
   letI hfin : Fintype ι := FiniteDimensional.fintypeBasisIndex B

Mathlib/Geometry/Euclidean/Altitude.lean

@@ -129,7 +129,7 @@ theorem affineSpan_pair_eq_altitude_iff {n : ℕ} [NeZero n] (s : Simplex ℝ P
       simpa using h
     · rw [finrank_direction_altitude, finrank_span_set_eq_card]
       · simp
-      · exact LinearIndepOn.id_singleton _ <| by simpa using hne
+      · exact .singleton <| by simpa using hne
 
 /-- The foot of an altitude is the orthogonal projection of a vertex of a simplex onto the
 opposite face. -/

Mathlib/LinearAlgebra/AffineSpace/Independent.lean

@@ -662,7 +662,7 @@ theorem affineIndependent_of_ne {p₁ p₂ : P} (h : p₁ ≠ p₂) : AffineInde
     · simp at hi
     · simp [i₁]
   haveI : Unique { x // x ≠ (0 : Fin 2) } := ⟨⟨i₁⟩, he'⟩
-  apply linearIndependent_unique
+  refine .of_subsingleton default ?_
   rw [he' default]
   simpa using h.symm
 

Mathlib/LinearAlgebra/Dimension/Constructions.lean

@@ -535,8 +535,8 @@ variable [StrongRankCondition F] [NoZeroSMulDivisors F E] [Nontrivial E]
 theorem Subalgebra.rank_bot : Module.rank F (⊥ : Subalgebra F E) = 1 :=
   (Subalgebra.toSubmoduleEquiv (⊥ : Subalgebra F E)).symm.rank_eq.trans <| by
     rw [Algebra.toSubmodule_bot, one_eq_span, rank_span_set, mk_singleton _]
-    letI := Module.nontrivial F E
-    exact LinearIndepOn.id_singleton _ one_ne_zero
+    have := Module.nontrivial F E
+    exact .singleton one_ne_zero
 
 @[simp]
 theorem Subalgebra.finrank_bot : finrank F (⊥ : Subalgebra F E) = 1 :=

Mathlib/LinearAlgebra/Dimension/RankNullity.lean

@@ -137,7 +137,7 @@ independent of the first one. -/
 theorem exists_linearIndependent_pair_of_one_lt_rank [StrongRankCondition R]
     [NoZeroSMulDivisors R M] (h : 1 < Module.rank R M) {x : M} (hx : x ≠ 0) :
     ∃ y, LinearIndependent R ![x, y] := by
-  obtain ⟨y, hy⟩ := exists_linearIndependent_snoc_of_lt_rank (linearIndependent_unique ![x] hx) h
+  obtain ⟨y, hy⟩ := exists_linearIndependent_snoc_of_lt_rank (.of_subsingleton (v := ![x]) 0 hx) h
   have : Fin.snoc ![x] y = ![x, y] := by simp [Fin.snoc, ← List.ofFn_inj]
   rw [this] at hy
   exact ⟨y, hy⟩

Mathlib/LinearAlgebra/FiniteDimensional/Basic.lean

@@ -532,11 +532,9 @@ section finrank_eq_one
 /-- A vector space with a nonzero vector `v` has dimension 1 iff `v` spans.
 -/
 theorem finrank_eq_one_iff_of_nonzero (v : V) (nz : v ≠ 0) :
-    finrank K V = 1 ↔ span K ({v} : Set V) = ⊤ :=
-  ⟨fun h => by simpa using (basisSingleton Unit h v nz).span_eq, fun s =>
-    finrank_eq_card_basis
-      (Basis.mk (LinearIndepOn.id_singleton _ nz)
-        (by simp [← s]))⟩
+    finrank K V = 1 ↔ span K ({v} : Set V) = ⊤ where
+  mp h := by simpa using (basisSingleton Unit h v nz).span_eq
+  mpr s := finrank_eq_card_basis <| .mk (.of_subsingleton (v := ![v]) 0 nz) <| by simp [← s]
 
 /-- A module with a nonzero vector `v` has dimension 1 iff every vector is a multiple of `v`.
 -/

Mathlib/LinearAlgebra/LinearIndependent/Basic.lean

@@ -272,16 +272,10 @@ alias LinearIndependent.linearCombination_ne_of_not_mem_support :=
 
 end Subtype
 
-section union
-
-open LinearMap Finsupp
-
 theorem LinearIndepOn.id_imageₛ {s : Set M} {f : M →ₗ[R] M'} (hs : LinearIndepOn R id s)
     (hf_inj : Set.InjOn f (span R s)) : LinearIndepOn R id (f '' s) :=
   id_image <| hs.map_injOn f (by simpa using hf_inj)
 
-end union
-
 theorem surjective_of_linearIndependent_of_span [Nontrivial R] (hv : LinearIndependent R v)
     (f : ι' ↪ ι) (hss : range v ⊆ span R (range (v ∘ f))) : Surjective f := by
   intro i
@@ -559,30 +553,21 @@ theorem linearIndependent_monoidHom (G : Type*) [MulOneClass G] (L : Type*) [Com
 end Module
 
 section Nontrivial
+variable [Ring R] [AddCommGroup M] [Module R M] [Nontrivial R] [NoZeroSMulDivisors R M]
+  {v : ι → M} {i : ι}
 
-variable [Ring R] [Nontrivial R] [AddCommGroup M]
-variable [Module R M] [NoZeroSMulDivisors R M]
-variable {s t : Set M}
-
-theorem linearIndependent_unique_iff (v : ι → M) [Unique ι] :
-    LinearIndependent R v ↔ v default ≠ 0 := by
-  simp only [linearIndependent_iff, Finsupp.linearCombination_unique, smul_eq_zero]
-  refine ⟨fun h hv => ?_, fun hv l hl => Finsupp.unique_ext <| hl.resolve_right hv⟩
-  have := h (Finsupp.single default 1) (Or.inr hv)
-  exact one_ne_zero (Finsupp.single_eq_zero.1 this)
+lemma linearIndependent_unique_iff [Unique ι] : LinearIndependent R v ↔ v default ≠ 0 := by
+  refine ⟨?_, .of_subsingleton _⟩
+  simpa [linearIndependent_iff, Finsupp.linearCombination_unique, Finsupp.ext_iff,
+    Unique.forall_iff, or_imp] using fun h hv ↦ by simpa using h (.single default 1) hv
 
+@[deprecated LinearIndependent.of_subsingleton (since := "2025-11-11")]
 alias ⟨_, linearIndependent_unique⟩ := linearIndependent_unique_iff
 
 variable (R) in
 @[simp]
-theorem linearIndepOn_singleton_iff {i : ι} {v : ι → M} : LinearIndepOn R v {i} ↔ v i ≠ 0 :=
-  ⟨fun h ↦ h.ne_zero rfl, fun h ↦ linearIndependent_unique _ h⟩
-
-alias ⟨_, LinearIndepOn.singleton⟩ := linearIndepOn_singleton_iff
-
-variable (R) in
-theorem LinearIndepOn.id_singleton {x : M} (hx : x ≠ 0) : LinearIndepOn R id {x} :=
-  linearIndependent_unique Subtype.val hx
+theorem linearIndepOn_singleton_iff : LinearIndepOn R v {i} ↔ v i ≠ 0 :=
+  ⟨fun h ↦ h.ne_zero rfl, .singleton⟩
 
 @[simp]
 theorem linearIndependent_subsingleton_index_iff [Subsingleton ι] (f : ι → M) :

Mathlib/LinearAlgebra/LinearIndependent/Defs.lean

@@ -702,9 +702,9 @@ end Semiring
 
 section Module
 
-variable {v : ι → M}
 variable [Ring R] [AddCommGroup M] [AddCommGroup M']
 variable [Module R M] [Module R M']
+variable {v : ι → M} {i : ι}
 
 theorem linearIndependent_iff_ker :
     LinearIndependent R v ↔ LinearMap.ker (Finsupp.linearCombination R v) = ⊥ :=
@@ -856,6 +856,29 @@ theorem linearIndependent_iff_eq_zero_of_smul_mem_span :
         simp [hij]
       · simp [hl]⟩
 
+/-- Version of `LinearIndependent.of_subsingleton` that works for the zero ring. -/
+lemma LinearIndependent.of_subsingleton' [Subsingleton ι] (i : ι)
+    (hi : ∀ r : R, r • v i = 0 → r = 0) : LinearIndependent R v := by
+  let := uniqueOfSubsingleton i
+  simpa [linearIndependent_iff, Finsupp.linearCombination_unique, Finsupp.ext_iff,
+    Unique.forall_iff] using fun _ ↦ hi _
+
+/-- Version of `LinearIndepOn.singleton` that works for the zero ring. -/
+@[simp]
+lemma LinearIndepOn.singleton' (hi : ∀ r : R, r • v i = 0 → r = 0) : LinearIndepOn R v {i} :=
+  LinearIndependent.of_subsingleton' ⟨i, rfl⟩ hi
+
+variable [NoZeroSMulDivisors R M]
+
+lemma LinearIndependent.of_subsingleton [Subsingleton ι] (i : ι) (hi : v i ≠ 0) :
+    LinearIndependent R v := .of_subsingleton' i (by simp [hi])
+
+lemma LinearIndepOn.singleton (hi : v i ≠ 0) : LinearIndepOn R v {i} := by simp [hi]
+
+variable (R) in
+@[deprecated LinearIndepOn.singleton (since := "2025-11-11")]
+lemma LinearIndepOn.id_singleton {x : M} (hx : x ≠ 0) : LinearIndepOn R id {x} := .singleton hx
+
 end Module
 
 /-!

Mathlib/LinearAlgebra/LinearIndependent/Lemmas.lean

@@ -480,6 +480,19 @@ lemma LinearMap.bijective_of_linearIndependent_of_span_eq_top {N : Type*} [AddCo
   rw [Set.range_comp, ← Submodule.map_span, hv, Submodule.map_top] at hsp
   rwa [← range_eq_top]
 
+/-- Version of `LinearIndepOn.insert` that works when the scalars are not a field. -/
+lemma LinearIndepOn.insert' {s : Set ι} {i : ι} (hs : LinearIndepOn R v s)
+    (hx : ∀ r : R, r • v i ∈ Submodule.span R (v '' s) → r = 0) :
+    LinearIndepOn R v (insert i s) := by
+  rw [← Set.union_singleton]
+  refine hs.union (.singleton' fun r hr ↦ hx _ <| by simp [hr]) ?_
+  simp +contextual [disjoint_span_singleton'', hx]
+
+/-- Version of `LinearIndepOn.id_insert` that works when the scalars are not a field. -/
+lemma LinearIndepOn.id_insert' {s : Set M} {x : M} (hs : LinearIndepOn R id s)
+    (hx : ∀ r : R, r • x ∈ Submodule.span R s → r = 0) : LinearIndepOn R id (insert x s) :=
+  hs.insert' <| by simpa
+
 end Module
 
 /-!
@@ -512,7 +525,7 @@ protected theorem LinearIndepOn.insert {s : Set ι} {x : ι} (hs : LinearIndepOn
     (hx : v x ∉ span K (v '' s)) : LinearIndepOn K v (insert x s) := by
   rw [← union_singleton]
   have x0 : v x ≠ 0 := fun h => hx (h ▸ zero_mem _)
-  apply hs.union (LinearIndepOn.singleton _ x0)
+  apply hs.union (LinearIndepOn.singleton x0)
   rwa [image_singleton, disjoint_span_singleton' x0]
 
 protected theorem LinearIndepOn.id_insert (hs : LinearIndepOn K id s) (hx : x ∉ span K s) :
@@ -589,9 +602,8 @@ theorem LinearIndepOn.notMem_span_iff_id {s : Set V} {a : V} (h : LinearIndepOn
 alias LinearIndepOn.not_mem_span_iff_id := LinearIndepOn.notMem_span_iff_id
 
 theorem linearIndepOn_id_pair {x y : V} (hx : x ≠ 0) (hy : ∀ a : K, a • x ≠ y) :
-    LinearIndepOn K id {x, y} :=
-  pair_comm y x ▸ (LinearIndepOn.id_singleton K hx).id_insert (x := y) <|
-    mt mem_span_singleton.1 <| not_exists.2 hy
+    LinearIndepOn K id {x, y} := by
+  rw [pair_comm]; exact .id_insert (.singleton hx) <| by simpa [mem_span_singleton]
 
 /-- `LinearIndepOn.pair_iff` is a version that works over arbitrary rings. -/
 theorem linearIndepOn_pair_iff {i j : ι} (v : ι → V) (hij : i ≠ j) (hi : v i ≠ 0) :

Mathlib/LinearAlgebra/Span/Basic.lean

@@ -589,6 +589,11 @@ theorem map_strict_mono_of_ker_inf_eq {f : F} (hab : p < p')
     (q : LinearMap.ker f ⊓ p = LinearMap.ker f ⊓ p') : Submodule.map f p < Submodule.map f p' :=
   map_strict_mono_or_ker_sup_lt_ker_sup f hab |>.resolve_right q.not_lt
 
+/-- Version of `disjoint_span_singleton` that works when the scalars are not a field. -/
+lemma disjoint_span_singleton'' {s : Submodule R M} {x : M} :
+    Disjoint s (R ∙ x) ↔ ∀ r : R, r • x ∈ s → r • x = 0 := by
+  rw [disjoint_comm]; simp +contextual [disjoint_def, mem_span_singleton]
+
 end Ring
 
 section DivisionRing
@@ -612,21 +617,14 @@ theorem covBy_span_singleton_sup {x : V} {s : Submodule K V} (h : x ∉ s) : Cov
   ⟨by simpa, (wcovBy_span_singleton_sup _ _).2⟩
 
 theorem disjoint_span_singleton : Disjoint s (K ∙ x) ↔ x ∈ s → x = 0 := by
-  refine disjoint_def.trans ⟨fun H hx => H x hx <| subset_span <| mem_singleton x, ?_⟩
-  intro H y hy hyx
-  obtain ⟨c, rfl⟩ := mem_span_singleton.1 hyx
-  by_cases hc : c = 0
-  · rw [hc, zero_smul]
-  · rw [s.smul_mem_iff hc] at hy
-    rw [H hy, smul_zero]
+  simpa +contextual [disjoint_span_singleton'', or_iff_not_imp_left, forall_swap (β := ¬_),
+    s.smul_mem_iff] using ⟨fun h ↦ h _ one_ne_zero, fun h _ _ ↦ h⟩
 
-theorem disjoint_span_singleton' (x0 : x ≠ 0) : Disjoint s (K ∙ x) ↔ x ∉ s :=
-  disjoint_span_singleton.trans ⟨fun h₁ h₂ => x0 (h₁ h₂), fun h₁ h₂ => (h₁ h₂).elim⟩
+theorem disjoint_span_singleton' (hx : x ≠ 0) : Disjoint s (K ∙ x) ↔ x ∉ s := by
+  simp [disjoint_span_singleton, hx]
 
 lemma disjoint_span_singleton_of_notMem (hx : x ∉ s) : Disjoint s (K ∙ x) := by
-  rw [disjoint_span_singleton]
-  intro h
-  contradiction
+  simp [disjoint_span_singleton, hx]
 
 @[deprecated (since := "2025-05-23")]
 alias disjoint_span_singleton_of_not_mem := disjoint_span_singleton_of_notMem