refactor(analysis/inner_product_space/pi_L2): change std_orthonormal_basis to type orthonormal_basis (#12253)

Co-authored-by: Daniel-Packer <62404584+Daniel-Packer@users.noreply.github.com>
Co-authored-by: Daniel Packer <62404584+Daniel-Packer@users.noreply.github.com>

Author: hrmacbeth

src/analysis/inner_product_space/orientation.lean

@@ -3,7 +3,7 @@ Copyright (c) 2022 Joseph Myers. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Myers
 -/
-import analysis.inner_product_space.projection
+import analysis.inner_product_space.pi_L2
 import linear_algebra.orientation
 
 /-!
@@ -37,7 +37,7 @@ protected def orientation.fin_orthonormal_basis {n : ℕ} (hn : 0 < n) (h : finr
 begin
   haveI := fin.pos_iff_nonempty.1 hn,
   haveI := finite_dimensional_of_finrank (h.symm ▸ hn : 0 < finrank ℝ E),
-  exact (fin_std_orthonormal_basis h).adjust_to_orientation x
+  exact (fin_std_orthonormal_basis h).to_basis.adjust_to_orientation x
 end
 
 /-- `orientation.fin_orthonormal_basis` is orthonormal. -/
@@ -47,7 +47,9 @@ protected lemma orientation.fin_orthonormal_basis_orthonormal {n : ℕ} (hn : 0
 begin
   haveI := fin.pos_iff_nonempty.1 hn,
   haveI := finite_dimensional_of_finrank (h.symm ▸ hn : 0 < finrank ℝ E),
-  exact (fin_std_orthonormal_basis_orthonormal h).orthonormal_adjust_to_orientation _
+  exact (show orthonormal ℝ (fin_std_orthonormal_basis h).to_basis, -- Note sure how to format this
+    by simp only [orthonormal_basis.coe_to_basis, orthonormal_basis.orthonormal]
+    ).orthonormal_adjust_to_orientation _
 end
 
 /-- `orientation.fin_orthonormal_basis` gives a basis with the required orientation. -/

src/analysis/inner_product_space/pi_L2.lean

@@ -27,14 +27,6 @@ defined in `analysis.inner_product_space.basic`); the lemma
 `submodule.sup_orthogonal_of_is_complete`, stating that for a complete subspace `K` of `E` we have
 `K ⊔ Kᗮ = ⊤`, is a typical example.
 
-The last section covers orthonormal bases, etc. The lemma
-`maximal_orthonormal_iff_orthogonal_complement_eq_bot` states that an orthonormal set in an inner
-product space is maximal, if and only the orthogonal complement of its span is trivial.
-Various consequences are stated for finite-dimensional `E`, including that a maximal orthonormal
-set is a basis (`maximal_orthonormal_iff_basis_of_finite_dimensional`); these consequences require
-the theory on the orthogonal complement developed earlier in this file.  For consequences in
-infinite dimension (Hilbert bases, etc.), see the file `analysis.inner_product_space.l2_space`.
-
 ## References
 
 The orthogonal projection construction is adapted from
@@ -1067,8 +1059,6 @@ end orthogonal_family
 
 section orthonormal_basis
 
-/-! ### Existence of orthonormal basis, etc. -/
-
 variables {𝕜 E} {v : set E}
 
 open finite_dimensional submodule set
@@ -1138,8 +1128,6 @@ begin
       exact hu.inner_finsupp_eq_zero hxv' hl }
 end
 
-section finite_dimensional
-
 variables [finite_dimensional 𝕜 E]
 
 /-- An orthonormal set in a finite-dimensional `inner_product_space` is maximal, if and only if it
@@ -1160,104 +1148,4 @@ begin
     rw [← h.span_eq, coe_h, hv_coe] }
 end
 
-/-- In a finite-dimensional `inner_product_space`, any orthonormal subset can be extended to an
-orthonormal basis. -/
-lemma exists_subset_is_orthonormal_basis
-  (hv : orthonormal 𝕜 (coe : v → E)) :
-  ∃ (u ⊇ v) (b : basis u 𝕜 E), orthonormal 𝕜 b ∧ ⇑b = coe :=
-begin
-  obtain ⟨u, hus, hu, hu_max⟩ := exists_maximal_orthonormal hv,
-  obtain ⟨b, hb⟩ := (maximal_orthonormal_iff_basis_of_finite_dimensional hu).mp hu_max,
-  exact ⟨u, hus, b, by rwa hb, hb⟩
-end
-
-variables (𝕜 E)
-
-/-- Index for an arbitrary orthonormal basis on a finite-dimensional `inner_product_space`. -/
-def orthonormal_basis_index : set E :=
-classical.some (exists_subset_is_orthonormal_basis (orthonormal_empty 𝕜 E))
-
-
-/-- A finite-dimensional `inner_product_space` has an orthonormal basis. -/
-def std_orthonormal_basis :
-  basis (orthonormal_basis_index 𝕜 E) 𝕜 E :=
-(exists_subset_is_orthonormal_basis (orthonormal_empty 𝕜 E)).some_spec.some_spec.some
-
-lemma std_orthonormal_basis_orthonormal :
-  orthonormal 𝕜 (std_orthonormal_basis 𝕜 E) :=
-(exists_subset_is_orthonormal_basis (orthonormal_empty 𝕜 E)).some_spec.some_spec.some_spec.1
-
-@[simp] lemma coe_std_orthonormal_basis :
-  ⇑(std_orthonormal_basis 𝕜 E) = coe :=
-(exists_subset_is_orthonormal_basis (orthonormal_empty 𝕜 E)).some_spec.some_spec.some_spec.2
-
-instance : fintype (orthonormal_basis_index 𝕜 E) :=
-@is_noetherian.fintype_basis_index _ _ _ _ _ _
-  (is_noetherian.iff_fg.2 infer_instance) (std_orthonormal_basis 𝕜 E)
-
-variables {𝕜 E}
-
-/-- An `n`-dimensional `inner_product_space` has an orthonormal basis indexed by `fin n`. -/
-def fin_std_orthonormal_basis {n : ℕ} (hn : finrank 𝕜 E = n) :
-  basis (fin n) 𝕜 E :=
-have h : fintype.card (orthonormal_basis_index 𝕜 E) = n,
-by rw [← finrank_eq_card_basis (std_orthonormal_basis 𝕜 E), hn],
-(std_orthonormal_basis 𝕜 E).reindex (fintype.equiv_fin_of_card_eq h)
-
-lemma fin_std_orthonormal_basis_orthonormal {n : ℕ} (hn : finrank 𝕜 E = n) :
-  orthonormal 𝕜 (fin_std_orthonormal_basis hn) :=
-suffices orthonormal 𝕜 (std_orthonormal_basis _ _ ∘ equiv.symm _),
-by { simp only [fin_std_orthonormal_basis, basis.coe_reindex], assumption }, -- simpa doesn't work?
-(std_orthonormal_basis_orthonormal 𝕜 E).comp _ (equiv.injective _)
-
-section subordinate_orthonormal_basis
-open direct_sum
-variables {n : ℕ} (hn : finrank 𝕜 E = n) {ι : Type*} [fintype ι] [decidable_eq ι]
-  {V : ι → submodule 𝕜 E} (hV : is_internal V)
-
-/-- Exhibit a bijection between `fin n` and the index set of a certain basis of an `n`-dimensional
-inner product space `E`.  This should not be accessed directly, but only via the subsequent API. -/
-@[irreducible] def direct_sum.is_internal.sigma_orthonormal_basis_index_equiv :
-  (Σ i, orthonormal_basis_index 𝕜 (V i)) ≃ fin n :=
-let b := hV.collected_basis (λ i, std_orthonormal_basis 𝕜 (V i)) in
-fintype.equiv_fin_of_card_eq $ (finite_dimensional.finrank_eq_card_basis b).symm.trans hn
-
-/-- An `n`-dimensional `inner_product_space` equipped with a decomposition as an internal direct
-sum has an orthonormal basis indexed by `fin n` and subordinate to that direct sum. -/
-@[irreducible] def direct_sum.is_internal.subordinate_orthonormal_basis :
-  basis (fin n) 𝕜 E :=
-(hV.collected_basis (λ i, std_orthonormal_basis 𝕜 (V i))).reindex
-  (hV.sigma_orthonormal_basis_index_equiv hn)
-
-/-- An `n`-dimensional `inner_product_space` equipped with a decomposition as an internal direct
-sum has an orthonormal basis indexed by `fin n` and subordinate to that direct sum. This function
-provides the mapping by which it is subordinate. -/
-def direct_sum.is_internal.subordinate_orthonormal_basis_index (a : fin n) : ι :=
-((hV.sigma_orthonormal_basis_index_equiv hn).symm a).1
-
-/-- The basis constructed in `orthogonal_family.subordinate_orthonormal_basis` is orthonormal. -/
-lemma direct_sum.is_internal.subordinate_orthonormal_basis_orthonormal
-  (hV' : @orthogonal_family 𝕜 _ _ _ _ (λ i, V i) _ (λ i, (V i).subtypeₗᵢ)) :
-  orthonormal 𝕜 (hV.subordinate_orthonormal_basis hn) :=
-begin
-  simp only [direct_sum.is_internal.subordinate_orthonormal_basis, basis.coe_reindex],
-  have : orthonormal 𝕜 (hV.collected_basis (λ i, std_orthonormal_basis 𝕜 (V i))) :=
-    hV.collected_basis_orthonormal hV' (λ i, std_orthonormal_basis_orthonormal 𝕜 (V i)),
-  exact this.comp _ (equiv.injective _),
-end
-
-/-- The basis constructed in `orthogonal_family.subordinate_orthonormal_basis` is subordinate to
-the `orthogonal_family` in question. -/
-lemma direct_sum.is_internal.subordinate_orthonormal_basis_subordinate (a : fin n) :
-  hV.subordinate_orthonormal_basis hn a ∈ V (hV.subordinate_orthonormal_basis_index hn a) :=
-by simpa only [direct_sum.is_internal.subordinate_orthonormal_basis, basis.coe_reindex]
-  using hV.collected_basis_mem (λ i, std_orthonormal_basis 𝕜 (V i))
-    ((hV.sigma_orthonormal_basis_index_equiv hn).symm a)
-
-attribute [irreducible] direct_sum.is_internal.subordinate_orthonormal_basis_index
-
-end subordinate_orthonormal_basis
-
-end finite_dimensional
-
 end orthonormal_basis

src/analysis/inner_product_space/projection.lean

@@ -179,30 +179,31 @@ finite-dimensional inner product space `E`.
 
 TODO Postcompose with a permutation so that these eigenvectors are listed in increasing order of
 eigenvalue. -/
-noncomputable def eigenvector_basis : basis (fin n) 𝕜 E :=
+noncomputable def eigenvector_basis : orthonormal_basis (fin n) 𝕜 E :=
 hT.direct_sum_is_internal.subordinate_orthonormal_basis hn
-
-lemma eigenvector_basis_orthonormal : orthonormal 𝕜 (hT.eigenvector_basis hn) :=
-hT.direct_sum_is_internal.subordinate_orthonormal_basis_orthonormal hn
   hT.orthogonal_family_eigenspaces'
 
 /-- The sequence of real eigenvalues associated to the standard orthonormal basis of eigenvectors
 for a self-adjoint operator `T` on `E`.
 
 TODO Postcompose with a permutation so that these eigenvalues are listed in increasing order. -/
 noncomputable def eigenvalues (i : fin n) : ℝ :=
-@is_R_or_C.re 𝕜 _ $ hT.direct_sum_is_internal.subordinate_orthonormal_basis_index hn i
+@is_R_or_C.re 𝕜 _ $
+  hT.direct_sum_is_internal.subordinate_orthonormal_basis_index hn i
+    hT.orthogonal_family_eigenspaces'
 
 lemma has_eigenvector_eigenvector_basis (i : fin n) :
   has_eigenvector T (hT.eigenvalues hn i) (hT.eigenvector_basis hn i) :=
 begin
   let v : E := hT.eigenvector_basis hn i,
-  let μ : 𝕜 := hT.direct_sum_is_internal.subordinate_orthonormal_basis_index hn i,
+  let μ : 𝕜 := hT.direct_sum_is_internal.subordinate_orthonormal_basis_index
+    hn i hT.orthogonal_family_eigenspaces',
   change has_eigenvector T (is_R_or_C.re μ) v,
   have key : has_eigenvector T μ v,
   { have H₁ : v ∈ eigenspace T μ,
-    { exact hT.direct_sum_is_internal.subordinate_orthonormal_basis_subordinate hn i },
-    have H₂ : v ≠ 0 := (hT.eigenvector_basis_orthonormal hn).ne_zero i,
+    { exact hT.direct_sum_is_internal.subordinate_orthonormal_basis_subordinate
+      hn i hT.orthogonal_family_eigenspaces' },
+    have H₂ : v ≠ 0 := by simpa using (hT.eigenvector_basis hn).to_basis.ne_zero i,
     exact ⟨H₁, H₂⟩ },
   have re_μ : ↑(is_R_or_C.re μ) = μ,
   { rw ← is_R_or_C.eq_conj_iff_re,
@@ -219,28 +220,25 @@ attribute [irreducible] eigenvector_basis eigenvalues
   T (hT.eigenvector_basis hn i) = (hT.eigenvalues hn i : 𝕜) • hT.eigenvector_basis hn i :=
 mem_eigenspace_iff.mp (hT.has_eigenvector_eigenvector_basis hn i).1
 
-/-- An isometry from an inner product space `E` to Euclidean space, induced by a choice of
-orthonormal basis of eigenvectors for a self-adjoint operator `T` on `E`. -/
-noncomputable def diagonalization_basis : E ≃ₗᵢ[𝕜] euclidean_space 𝕜 (fin n) :=
-((hT.eigenvector_basis hn).to_orthonormal_basis (hT.eigenvector_basis_orthonormal hn)).repr
-
-@[simp] lemma diagonalization_basis_symm_apply (w : euclidean_space 𝕜 (fin n)) :
-  (hT.diagonalization_basis hn).symm w = ∑ i, w i • hT.eigenvector_basis hn i :=
-by simp [diagonalization_basis]
-
 /-- *Diagonalization theorem*, *spectral theorem*; version 2: A self-adjoint operator `T` on a
 finite-dimensional inner product space `E` acts diagonally on the identification of `E` with
 Euclidean space induced by an orthonormal basis of eigenvectors of `T`. -/
 lemma diagonalization_basis_apply_self_apply (v : E) (i : fin n) :
-  hT.diagonalization_basis hn (T v) i = hT.eigenvalues hn i * hT.diagonalization_basis hn v i :=
+  (hT.eigenvector_basis hn).repr (T v) i =
+    hT.eigenvalues hn i * (hT.eigenvector_basis hn).repr v i :=
 begin
   suffices : ∀ w : euclidean_space 𝕜 (fin n),
-    T ((hT.diagonalization_basis hn).symm w)
-    = (hT.diagonalization_basis hn).symm (λ i, hT.eigenvalues hn i * w i),
-  { simpa [-diagonalization_basis_symm_apply] using
-      congr_arg (λ v, hT.diagonalization_basis hn v i) (this (hT.diagonalization_basis hn v)) },
+    T ((hT.eigenvector_basis hn).repr.symm w)
+    = (hT.eigenvector_basis hn).repr.symm (λ i, hT.eigenvalues hn i * w i),
+  { simpa [orthonormal_basis.sum_repr_symm] using
+      congr_arg (λ v, (hT.eigenvector_basis hn).repr v i)
+        (this ((hT.eigenvector_basis hn).repr v)) },
   intros w,
-  simp [mul_comm, mul_smul],
+  simp_rw [← orthonormal_basis.sum_repr_symm, linear_map.map_sum,
+    linear_map.map_smul, apply_eigenvector_basis],
+  apply fintype.sum_congr,
+  intros a,
+  rw [smul_smul, mul_comm],
 end
 
 end version2

src/analysis/inner_product_space/spectrum.lean

@@ -353,6 +353,47 @@ variables (x y : pi_Lp p β) (x' y' : Π i, β i) (i : ι)
 @[simp] lemma smul_apply : (c • x) i = c • x i := rfl
 @[simp] lemma neg_apply : (-x) i = - (x i) := rfl
 
+variables {ι' : Type*}
+variables [fintype ι']
+
+variables (p 𝕜) (E : Type*) [normed_group E] [normed_space 𝕜 E]
+
+/-- An equivalence of finite domains induces a linearly isometric equivalence of finitely supported
+functions-/
+def _root_.linear_isometry_equiv.pi_Lp_congr_left (e : ι ≃ ι') :
+  pi_Lp p (λ i : ι, E) ≃ₗᵢ[𝕜] pi_Lp p (λ i : ι', E) :=
+{ to_linear_equiv := linear_equiv.Pi_congr_left' 𝕜 (λ i : ι, E) e,
+  norm_map' :=
+  begin
+    intro x,
+    simp only [norm],
+    simp_rw linear_equiv.Pi_congr_left'_apply 𝕜 (λ i : ι, E) e x _,
+    congr,
+    rw fintype.sum_equiv (e.symm),
+    exact λ i, rfl,
+  end, }
+
+variables {p 𝕜 E}
+
+@[simp] lemma _root_.linear_isometry_equiv.pi_Lp_congr_left_apply
+  (e : ι ≃ ι') (v : pi_Lp p (λ i : ι, E)) :
+  linear_isometry_equiv.pi_Lp_congr_left p 𝕜 E e v = equiv.Pi_congr_left' (λ i : ι, E) e v :=
+rfl
+
+@[simp] lemma _root_.linear_isometry_equiv.pi_Lp_congr_left_symm (e : ι ≃ ι') :
+  (linear_isometry_equiv.pi_Lp_congr_left p 𝕜 E e).symm
+    = (linear_isometry_equiv.pi_Lp_congr_left p 𝕜 E e.symm) :=
+linear_isometry_equiv.ext $ λ x, rfl
+
+@[simp] lemma _root_.linear_isometry_equiv.pi_Lp_congr_left_single
+  [decidable_eq ι] [decidable_eq ι'] (e : ι ≃ ι') (i : ι) (v : E) :
+  linear_isometry_equiv.pi_Lp_congr_left p 𝕜 E e (pi.single i v) = pi.single (e i) v :=
+begin
+  funext x,
+  simp [linear_isometry_equiv.pi_Lp_congr_left, linear_equiv.Pi_congr_left', equiv.Pi_congr_left',
+    pi.single, function.update, equiv.symm_apply_eq],
+end
+
 @[simp] lemma equiv_zero : pi_Lp.equiv p β 0 = 0 := rfl
 @[simp] lemma equiv_symm_zero : (pi_Lp.equiv p β).symm 0 = 0 := rfl
 

src/analysis/normed_space/pi_Lp.lean

@@ -294,8 +294,8 @@ from `(ℝ ∙ v)ᗮ` to the Euclidean space. -/
 def stereographic' (n : ℕ) [fact (finrank ℝ E = n + 1)] (v : sphere (0:E) 1) :
   local_homeomorph (sphere (0:E) 1) (euclidean_space ℝ (fin n)) :=
 (stereographic (norm_eq_of_mem_sphere v)) ≫ₕ
-(linear_isometry_equiv.from_orthogonal_span_singleton n
-  (ne_zero_of_mem_unit_sphere v)).to_homeomorph.to_local_homeomorph
+(orthonormal_basis.from_orthogonal_span_singleton n
+  (ne_zero_of_mem_unit_sphere v)).repr.to_homeomorph.to_local_homeomorph
 
 @[simp] lemma stereographic'_source {n : ℕ} [fact (finrank ℝ E = n + 1)] (v : sphere (0:E) 1) :
   (stereographic' n v).source = {v}ᶜ :=
@@ -326,8 +326,8 @@ lemma stereographic'_symm_apply {n : ℕ} [fact (finrank ℝ E = n + 1)]
     (v : sphere (0:E) 1) (x : euclidean_space ℝ (fin n)) :
   ((stereographic' n v).symm x : E) =
     let U : (ℝ ∙ (v:E))ᗮ ≃ₗᵢ[ℝ] euclidean_space ℝ (fin n) :=
-      linear_isometry_equiv.from_orthogonal_span_singleton n
-        (ne_zero_of_mem_unit_sphere v) in
+      (orthonormal_basis.from_orthogonal_span_singleton n
+        (ne_zero_of_mem_unit_sphere v)).repr in
     ((∥(U.symm x : E)∥ ^ 2 + 4)⁻¹ • (4 : ℝ) • (U.symm x : E) +
       (∥(U.symm x : E)∥ ^ 2 + 4)⁻¹ • (∥(U.symm x : E)∥ ^ 2 - 4) • v) :=
 by simp [real_inner_comm, stereographic, stereographic', ← submodule.coe_norm]
@@ -341,12 +341,16 @@ instance {n : ℕ} [fact (finrank ℝ E = n + 1)] :
 smooth_manifold_with_corners_of_cont_diff_on (𝓡 n) (sphere (0:E) 1)
 begin
   rintros _ _ ⟨v, rfl⟩ ⟨v', rfl⟩,
-  let U : (ℝ ∙ (v:E))ᗮ ≃ₗᵢ[ℝ] euclidean_space ℝ (fin n) :=
-    linear_isometry_equiv.from_orthogonal_span_singleton n
-      (ne_zero_of_mem_unit_sphere v),
-  let U' : (ℝ ∙ (v':E))ᗮ ≃ₗᵢ[ℝ] euclidean_space ℝ (fin n) :=
-    linear_isometry_equiv.from_orthogonal_span_singleton n
-      (ne_zero_of_mem_unit_sphere v'),
+  let U := -- Removed type ascription, and this helped for some reason with timeout issues?
+    (orthonormal_basis.from_orthogonal_span_singleton n
+      (ne_zero_of_mem_unit_sphere v)).repr,
+  let U' :=-- Removed type ascription, and this helped for some reason with timeout issues?
+    (orthonormal_basis.from_orthogonal_span_singleton n
+      (ne_zero_of_mem_unit_sphere v')).repr,
+  have hUv : stereographic' n v = (stereographic (norm_eq_of_mem_sphere v)) ≫ₕ
+    U.to_homeomorph.to_local_homeomorph := rfl,
+  have hU'v' : stereographic' n v' = (stereographic (norm_eq_of_mem_sphere v')).trans
+    U'.to_homeomorph.to_local_homeomorph := rfl,
   have H₁ := U'.cont_diff.comp_cont_diff_on cont_diff_on_stereo_to_fun,
   have H₂ := (cont_diff_stereo_inv_fun_aux.comp
       (ℝ ∙ (v:E))ᗮ.subtypeL.cont_diff).comp U.symm.cont_diff,
@@ -363,8 +367,9 @@ begin
   split,
   { exact continuous_subtype_coe },
   { intros v _,
-    let U : (ℝ ∙ ((-v):E))ᗮ ≃ₗᵢ[ℝ] euclidean_space ℝ (fin n) :=
-      linear_isometry_equiv.from_orthogonal_span_singleton n (ne_zero_of_mem_unit_sphere (-v)),
+    let U := -- Again, removing type ascription...
+      (orthonormal_basis.from_orthogonal_span_singleton n
+        (ne_zero_of_mem_unit_sphere (-v))).repr,
     exact ((cont_diff_stereo_inv_fun_aux.comp
       (ℝ ∙ ((-v):E))ᗮ.subtypeL.cont_diff).comp U.symm.cont_diff).cont_diff_on }
 end
@@ -383,8 +388,8 @@ begin
   rw cont_mdiff_iff_target,
   refine ⟨continuous_induced_rng hf.continuous, _⟩,
   intros v,
-  let U : (ℝ ∙ ((-v):E))ᗮ ≃ₗᵢ[ℝ] euclidean_space ℝ (fin n) :=
-    (linear_isometry_equiv.from_orthogonal_span_singleton n (ne_zero_of_mem_unit_sphere (-v))),
+  let U := -- Again, removing type ascription... Weird that this helps!
+    (orthonormal_basis.from_orthogonal_span_singleton n (ne_zero_of_mem_unit_sphere (-v))).repr,
   have h : cont_diff_on ℝ ⊤ _ set.univ :=
     U.cont_diff.cont_diff_on,
   have H₁ := (h.comp' cont_diff_on_stereo_to_fun).cont_mdiff_on,

src/geometry/manifold/instances/sphere.lean

@@ -314,6 +314,11 @@ begin
   apply cardinal.nat_lt_aleph_0,
 end
 
+lemma _root_.linear_independent.finite {K : Type*} {V : Type*} [division_ring K] [add_comm_group V]
+  [module K V] [finite_dimensional K V] {b : set V} (h : linear_independent K (λ (x:b), (x:V))) :
+  b.finite :=
+cardinal.lt_aleph_0_iff_set_finite.mp (finite_dimensional.lt_aleph_0_of_linear_independent h)
+
 lemma not_linear_independent_of_infinite {ι : Type w} [inf : infinite ι] [finite_dimensional K V]
   (v : ι → V) : ¬ linear_independent K v :=
 begin