ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>DivisionRing k<VAR>AddCommGroup V<VAR>Module k V<VAR>AffineSpace V P<VAR>s : Set P<GOAL>Collinear k s ↔ Module.rank k ↥(vectorSpan k s) ≤ 1
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>DivisionRing k<VAR>AddCommGroup V<VAR>Module k V<VAR>AffineSpace V P<VAR>s : Set P<VAR>FiniteDimensional k ↥(vectorSpan k s)<GOAL>Collinear k s ↔ FiniteDimensional.finrank k ↥(vectorSpan k s) ≤ 1
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>DivisionRing k<VAR>AddCommGroup V<VAR>Module k V<VAR>AffineSpace V P<VAR>s₁ s₂ : Set P<VAR>hs : s₁ ⊆ s₂<VAR>h : Collinear k s₂<GOAL>Collinear k s₁
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>DivisionRing k<VAR>AddCommGroup V<VAR>Module k V<VAR>AffineSpace V P<VAR>s : Set P<VAR>h : Collinear k s<GOAL>FiniteDimensional k ↥(vectorSpan k s)
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>DivisionRing k<VAR>AddCommGroup V<VAR>Module k V<VAR>AffineSpace V P<VAR>s : Set P<VAR>h : Collinear k s<GOAL>FiniteDimensional k ↥(affineSpan k s).direction
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>DivisionRing k<VAR>AddCommGroup V<VAR>Module k V<VAR>AffineSpace V P<GOAL>Collinear k ∅
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>DivisionRing k<VAR>AddCommGroup V<VAR>Module k V<VAR>AffineSpace V P<VAR>p : P<GOAL>Collinear k {p}
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>DivisionRing k<VAR>AddCommGroup V<VAR>Module k V<VAR>AffineSpace V P<VAR>s : Set P<VAR>p₀ : P<VAR>h : p₀ ∈ s<GOAL>Collinear k s ↔ ∃ v, ∀ p ∈ s, ∃ r, p = r • v +ᵥ p₀
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>DivisionRing k<VAR>AddCommGroup V<VAR>Module k V<VAR>AffineSpace V P<VAR>s : Set P<GOAL>Collinear k s ↔ ∃ p₀ v, ∀ p ∈ s, ∃ r, p = r • v +ᵥ p₀
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>DivisionRing k<VAR>AddCommGroup V<VAR>Module k V<VAR>AffineSpace V P<VAR>p₁ p₂ : P<GOAL>Collinear k {p₁, p₂}
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>DivisionRing k<VAR>AddCommGroup V<VAR>Module k V<VAR>AffineSpace V P<VAR>p : Fin 3 → P<GOAL>AffineIndependent k p ↔ ¬Collinear k (Set.range p)
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>DivisionRing k<VAR>AddCommGroup V<VAR>Module k V<VAR>AffineSpace V P<VAR>p : Fin 3 → P<GOAL>Collinear k (Set.range p) ↔ ¬AffineIndependent k p
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>DivisionRing k<VAR>AddCommGroup V<VAR>Module k V<VAR>AffineSpace V P<VAR>p₁ p₂ p₃ : P<GOAL>AffineIndependent k ![p₁, p₂, p₃] ↔ ¬Collinear k {p₁, p₂, p₃}
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>DivisionRing k<VAR>AddCommGroup V<VAR>Module k V<VAR>AffineSpace V P<VAR>p₁ p₂ p₃ : P<GOAL>Collinear k {p₁, p₂, p₃} ↔ ¬AffineIndependent k ![p₁, p₂, p₃]
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>DivisionRing k<VAR>AddCommGroup V<VAR>Module k V<VAR>AffineSpace V P<VAR>p : Fin 3 → P<VAR>i₁ i₂ i₃ : Fin 3<VAR>h₁₂ : i₁ ≠ i₂<VAR>h₁₃ : i₁ ≠ i₃<VAR>h₂₃ : i₂ ≠ i₃<GOAL>AffineIndependent k p ↔ ¬Collinear k {p i₁, p i₂, p i₃}
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>DivisionRing k<VAR>AddCommGroup V<VAR>Module k V<VAR>AffineSpace V P<VAR>p : Fin 3 → P<VAR>i₁ i₂ i₃ : Fin 3<VAR>h₁₂ : i₁ ≠ i₂<VAR>h₁₃ : i₁ ≠ i₃<VAR>h₂₃ : i₂ ≠ i₃<GOAL>Collinear k {p i₁, p i₂, p i₃} ↔ ¬AffineIndependent k p
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>DivisionRing k<VAR>AddCommGroup V<VAR>Module k V<VAR>AffineSpace V P<VAR>p₁ p₂ p₃ : P<VAR>h : ¬Collinear k {p₁, p₂, p₃}<GOAL>p₁ ≠ p₂
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>DivisionRing k<VAR>AddCommGroup V<VAR>Module k V<VAR>AffineSpace V P<VAR>p₁ p₂ p₃ : P<VAR>h : ¬Collinear k {p₁, p₂, p₃}<GOAL>p₁ ≠ p₃
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>DivisionRing k<VAR>AddCommGroup V<VAR>Module k V<VAR>AffineSpace V P<VAR>p₁ p₂ p₃ : P<VAR>h : ¬Collinear k {p₁, p₂, p₃}<GOAL>p₂ ≠ p₃
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>DivisionRing k<VAR>AddCommGroup V<VAR>Module k V<VAR>AffineSpace V P<VAR>s : Set P<VAR>h : Collinear k s<VAR>p₁ p₂ p₃ : P<VAR>hp₁ : p₁ ∈ s<VAR>hp₂ : p₂ ∈ s<VAR>hp₃ : p₃ ∈ s<VAR>hp₁p₂ : p₁ ≠ p₂<GOAL>p₃ ∈ affineSpan k {p₁, p₂}
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>DivisionRing k<VAR>AddCommGroup V<VAR>Module k V<VAR>AffineSpace V P<VAR>s : Set P<VAR>h : Collinear k s<VAR>p₁ p₂ : P<VAR>hp₁ : p₁ ∈ s<VAR>hp₂ : p₂ ∈ s<VAR>hp₁p₂ : p₁ ≠ p₂<GOAL>affineSpan k {p₁, p₂} = affineSpan k s
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>DivisionRing k<VAR>AddCommGroup V<VAR>Module k V<VAR>AffineSpace V P<VAR>s : Set P<VAR>h : Collinear k s<VAR>p₁ p₂ p₃ : P<VAR>hp₂ : p₂ ∈ s<VAR>hp₃ : p₃ ∈ s<VAR>hp₂p₃ : p₂ ≠ p₃<GOAL>Collinear k (insert p₁ s) ↔ Collinear k {p₁, p₂, p₃}
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>DivisionRing k<VAR>AddCommGroup V<VAR>Module k V<VAR>AffineSpace V P<VAR>s : Set P<VAR>p : P<VAR>h : p ∈ affineSpan k s<GOAL>Collinear k (insert p s) ↔ Collinear k s
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>DivisionRing k<VAR>AddCommGroup V<VAR>Module k V<VAR>AffineSpace V P<VAR>p₁ p₂ p₃ : P<VAR>h : p₁ ∈ affineSpan k {p₂, p₃}<GOAL>Collinear k {p₁, p₂, p₃}
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>DivisionRing k<VAR>AddCommGroup V<VAR>Module k V<VAR>AffineSpace V P<VAR>p₁ p₂ p₃ p₄ : P<VAR>h₁ : p₁ ∈ affineSpan k {p₃, p₄}<VAR>h₂ : p₂ ∈ affineSpan k {p₃, p₄}<GOAL>Collinear k {p₁, p₂, p₃, p₄}
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>DivisionRing k<VAR>AddCommGroup V<VAR>Module k V<VAR>AffineSpace V P<VAR>p₁ p₂ p₃ p₄ p₅ : P<VAR>h₁ : p₁ ∈ affineSpan k {p₄, p₅}<VAR>h₂ : p₂ ∈ affineSpan k {p₄, p₅}<VAR>h₃ : p₃ ∈ affineSpan k {p₄, p₅}<GOAL>Collinear k {p₁, p₂, p₃, p₄, p₅}
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>DivisionRing k<VAR>AddCommGroup V<VAR>Module k V<VAR>AffineSpace V P<VAR>p₁ p₂ p₃ p₄ p₅ : P<VAR>h₁ : p₁ ∈ affineSpan k {p₄, p₅}<VAR>h₂ : p₂ ∈ affineSpan k {p₄, p₅}<VAR>h₃ : p₃ ∈ affineSpan k {p₄, p₅}<GOAL>Collinear k {p₁, p₂, p₃, p₄}
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>DivisionRing k<VAR>AddCommGroup V<VAR>Module k V<VAR>AffineSpace V P<VAR>p₁ p₂ p₃ p₄ p₅ : P<VAR>h₁ : p₁ ∈ affineSpan k {p₄, p₅}<VAR>h₂ : p₂ ∈ affineSpan k {p₄, p₅}<VAR>h₃ : p₃ ∈ affineSpan k {p₄, p₅}<GOAL>Collinear k {p₁, p₂, p₃}
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>DivisionRing k<VAR>AddCommGroup V<VAR>Module k V<VAR>AffineSpace V P<VAR>s : Set P<VAR>h : Coplanar k s<GOAL>FiniteDimensional k ↥(vectorSpan k s)
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>DivisionRing k<VAR>AddCommGroup V<VAR>Module k V<VAR>AffineSpace V P<VAR>s : Set P<VAR>h : Coplanar k s<GOAL>FiniteDimensional k ↥(affineSpan k s).direction
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>DivisionRing k<VAR>AddCommGroup V<VAR>Module k V<VAR>AffineSpace V P<VAR>s : Set P<VAR>FiniteDimensional k ↥(vectorSpan k s)<GOAL>Coplanar k s ↔ FiniteDimensional.finrank k ↥(vectorSpan k s) ≤ 2
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>DivisionRing k<VAR>AddCommGroup V<VAR>Module k V<VAR>AffineSpace V P<VAR>s₁ s₂ : Set P<VAR>hs : s₁ ⊆ s₂<VAR>h : Coplanar k s₂<GOAL>Coplanar k s₁
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>DivisionRing k<VAR>AddCommGroup V<VAR>Module k V<VAR>AffineSpace V P<VAR>s : Set P<VAR>h : Collinear k s<GOAL>Coplanar k s
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>DivisionRing k<VAR>AddCommGroup V<VAR>Module k V<VAR>AffineSpace V P<GOAL>Coplanar k ∅
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>DivisionRing k<VAR>AddCommGroup V<VAR>Module k V<VAR>AffineSpace V P<VAR>p : P<GOAL>Coplanar k {p}
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>DivisionRing k<VAR>AddCommGroup V<VAR>Module k V<VAR>AffineSpace V P<VAR>p₁ p₂ : P<GOAL>Coplanar k {p₁, p₂}
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>DivisionRing k<VAR>AddCommGroup V<VAR>Module k V<VAR>AffineSpace V P<VAR>s : Set P<VAR>p : P<VAR>h : p ∈ affineSpan k s<GOAL>Coplanar k (insert p s) ↔ Coplanar k s
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>DivisionRing k<VAR>AddCommGroup V<VAR>Module k V<VAR>AffineSpace V P<VAR>s : AffineSubspace k P<VAR>p : P<GOAL>FiniteDimensional.finrank k ↥(vectorSpan k (insert p ↑s)) ≤ FiniteDimensional.finrank k ↥s.direction + 1
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>DivisionRing k<VAR>AddCommGroup V<VAR>Module k V<VAR>AffineSpace V P<VAR>s : Set P<VAR>p : P<GOAL>FiniteDimensional.finrank k ↥(vectorSpan k (insert p s)) ≤ FiniteDimensional.finrank k ↥(vectorSpan k s) + 1
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>DivisionRing k<VAR>AddCommGroup V<VAR>Module k V<VAR>AffineSpace V P<VAR>s : Set P<VAR>h : Collinear k s<VAR>p : P<GOAL>Coplanar k (insert p s)
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>DivisionRing k<VAR>AddCommGroup V<VAR>Module k V<VAR>AffineSpace V P<VAR>s : Set P<VAR>h : FiniteDimensional.finrank k V = 2<GOAL>Coplanar k s
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>DivisionRing k<VAR>AddCommGroup V<VAR>Module k V<VAR>AffineSpace V P<VAR>s : Set P<VAR>h : Fact (FiniteDimensional.finrank k V = 2)<GOAL>Coplanar k s
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>DivisionRing k<VAR>AddCommGroup V<VAR>Module k V<VAR>AffineSpace V P<VAR>p₁ p₂ p₃ : P<GOAL>Coplanar k {p₁, p₂, p₃}
<VAR>ι : Type u₁<VAR>k : Type u₂<VAR>V : Type u₃<VAR>P : Type u₄<VAR>AddCommGroup V<VAR>AffineSpace V P<VAR>DivisionRing k<VAR>Module k V<VAR>Finite ι<VAR>b : AffineBasis ι k P<GOAL>FiniteDimensional k V
<VAR>ι : Type u₁<VAR>k : Type u₂<VAR>V : Type u₃<VAR>P : Type u₄<VAR>AddCommGroup V<VAR>AffineSpace V P<VAR>DivisionRing k<VAR>Module k V<VAR>FiniteDimensional k V<VAR>b : AffineBasis ι k P<GOAL>Finite ι
<VAR>ι : Type u₁<VAR>k : Type u₂<VAR>V : Type u₃<VAR>P : Type u₄<VAR>AddCommGroup V<VAR>AffineSpace V P<VAR>DivisionRing k<VAR>Module k V<VAR>FiniteDimensional k V<VAR>s : Set ι<VAR>b : AffineBasis (↑s) k P<GOAL>s.Finite
<VAR>ι : Type u₁<VAR>k : Type u₂<VAR>V : Type u₃<VAR>P : Type u₄<VAR>AddCommGroup V<VAR>AffineSpace V P<VAR>DivisionRing k<VAR>Module k V<VAR>Fintype ι<VAR>b : AffineBasis ι k P<GOAL>Fintype.card ι = FiniteDimensional.finrank k V + 1
<VAR>ι : Type u₁<VAR>k : Type u₂<VAR>V : Type u₃<VAR>P : Type u₄<VAR>AddCommGroup V<VAR>AffineSpace V P<VAR>DivisionRing k<VAR>Module k V<VAR>Fintype ι<VAR>FiniteDimensional k V<VAR>h : Fintype.card ι = FiniteDimensional.finrank k V + 1<GOAL>Nonempty (AffineBasis ι k P)
<VAR>K : Type u_1<VAR>n : Type u_2<VAR>NormedField K<VAR>Fintype n<VAR>DecidableEq n<VAR>A : Matrix n n K<VAR>μ : K<VAR>hμ : Module.End.HasEigenvalue (Matrix.toLin' A) μ<GOAL>∃ k, μ ∈ Metric.closedBall (A k k) (∑ j ∈ Finset.univ.erase k, ‖A k j‖)
<VAR>K : Type u_1<VAR>n : Type u_2<VAR>NormedField K<VAR>Fintype n<VAR>DecidableEq n<VAR>A : Matrix n n K<VAR>h : ∀ (k : n), ∑ j ∈ Finset.univ.erase k, ‖A k j‖ < ‖A k k‖<GOAL>A.det ≠ 0
<VAR>K : Type u_1<VAR>n : Type u_2<VAR>NormedField K<VAR>Fintype n<VAR>DecidableEq n<VAR>A : Matrix n n K<VAR>h : ∀ (k : n), ∑ i ∈ Finset.univ.erase k, ‖A i k‖ < ‖A k k‖<GOAL>A.det ≠ 0
<VAR>α : Type u_1<VAR>n : Type u_4<VAR>Sub n<VAR>v : n → α<VAR>i j : n<GOAL>Matrix.circulant v i j = v (i - j)
<VAR>α : Type u_1<VAR>n : Type u_4<VAR>AddGroup n<VAR>v : n → α<VAR>i : n<GOAL>Matrix.circulant v i 0 = v i
<VAR>α : Type u_1<VAR>n : Type u_4<VAR>AddGroup n<GOAL>Function.Injective Matrix.circulant
<VAR>α : Type u_1<VAR>n : ℕ<GOAL>Function.Injective fun v => Matrix.circulant v
<VAR>α : Type u_1<VAR>n : Type u_4<VAR>AddGroup n<VAR>v w : n → α<GOAL>Matrix.circulant v = Matrix.circulant w ↔ v = w
<VAR>α : Type u_1<VAR>n : ℕ<VAR>v w : Fin n → α<GOAL>Matrix.circulant v = Matrix.circulant w ↔ v = w
<VAR>α : Type u_1<VAR>n : Type u_4<VAR>AddGroup n<VAR>v : n → α<GOAL>(Matrix.circulant v).transpose = Matrix.circulant fun i => v (-i)
<VAR>α : Type u_1<VAR>n : Type u_4<VAR>Star α<VAR>AddGroup n<VAR>v : n → α<GOAL>(Matrix.circulant v).conjTranspose = Matrix.circulant (star fun i => v (-i))
<VAR>α : Type u_1<VAR>n : ℕ<VAR>v : Fin n → α<GOAL>(Matrix.circulant v).transpose = Matrix.circulant fun i => v (-i)
<VAR>α : Type u_1<VAR>Star α<VAR>n : ℕ<VAR>v : Fin n → α<GOAL>(Matrix.circulant v).conjTranspose = Matrix.circulant (star fun i => v (-i))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n : Type u_4<VAR>Sub n<VAR>v : n → α<VAR>f : α → β<GOAL>(Matrix.circulant v).map f = Matrix.circulant fun i => f (v i)
<VAR>α : Type u_1<VAR>n : Type u_4<VAR>Neg α<VAR>Sub n<VAR>v : n → α<GOAL>Matrix.circulant (-v) = -Matrix.circulant v
<VAR>α : Type u_6<VAR>n : Type u_7<VAR>Zero α<VAR>Sub n<GOAL>Matrix.circulant 0 = 0
<VAR>α : Type u_1<VAR>n : Type u_4<VAR>Add α<VAR>Sub n<VAR>v w : n → α<GOAL>Matrix.circulant (v + w) = Matrix.circulant v + Matrix.circulant w
<VAR>α : Type u_1<VAR>n : Type u_4<VAR>Sub α<VAR>Sub n<VAR>v w : n → α<GOAL>Matrix.circulant (v - w) = Matrix.circulant v - Matrix.circulant w
<VAR>α : Type u_1<VAR>n : Type u_4<VAR>Semiring α<VAR>Fintype n<VAR>AddGroup n<VAR>v w : n → α<GOAL>Matrix.circulant v * Matrix.circulant w = Matrix.circulant ((Matrix.circulant v).mulVec w)
<VAR>α : Type u_1<VAR>Semiring α<VAR>n : ℕ<VAR>v w : Fin n → α<GOAL>Matrix.circulant v * Matrix.circulant w = Matrix.circulant ((Matrix.circulant v).mulVec w)
<VAR>α : Type u_1<VAR>n : Type u_4<VAR>CommSemigroup α<VAR>AddCommMonoid α<VAR>Fintype n<VAR>AddCommGroup n<VAR>v w : n → α<GOAL>Matrix.circulant v * Matrix.circulant w = Matrix.circulant w * Matrix.circulant v
<VAR>α : Type u_1<VAR>CommSemigroup α<VAR>AddCommMonoid α<VAR>n : ℕ<VAR>v w : Fin n → α<GOAL>Matrix.circulant v * Matrix.circulant w = Matrix.circulant w * Matrix.circulant v
<VAR>α : Type u_1<VAR>n : Type u_4<VAR>R : Type u_5<VAR>Sub n<VAR>SMul R α<VAR>k : R<VAR>v : n → α<GOAL>Matrix.circulant (k • v) = k • Matrix.circulant v
<VAR>α : Type u_6<VAR>n : Type u_7<VAR>Zero α<VAR>One α<VAR>DecidableEq n<VAR>AddGroup n<GOAL>Matrix.circulant (Pi.single 0 1) = 1
<VAR>α : Type u_1<VAR>n : Type u_6<VAR>Semiring α<VAR>DecidableEq n<VAR>AddGroup n<VAR>Fintype n<VAR>a : α<GOAL>Matrix.circulant (Pi.single 0 a) = (Matrix.scalar n) a
<VAR>α : Type u_6<VAR>Zero α<VAR>One α<VAR>n : ℕ<GOAL>(Matrix.circulant fun i => if ↑i = 0 then 1 else 0) = 1
<VAR>α : Type u_1<VAR>n : Type u_4<VAR>AddGroup n<VAR>v : n → α<GOAL>(Matrix.circulant v).IsSymm ↔ ∀ (i : n), v (-i) = v i
<VAR>α : Type u_1<VAR>n : ℕ<VAR>v : Fin n → α<GOAL>(Matrix.circulant v).IsSymm ↔ ∀ (i : Fin n), v (-i) = v i
<VAR>α : Type u_1<VAR>n : Type u_4<VAR>AddGroup n<VAR>v : n → α<VAR>h : (Matrix.circulant v).IsSymm<VAR>i : n<GOAL>v (-i) = v i
<VAR>α : Type u_1<VAR>n : ℕ<VAR>v : Fin n → α<VAR>h : (Matrix.circulant v).IsSymm<VAR>i : Fin n<GOAL>v (-i) = v i
<VAR>ι : Type u'<VAR>R : Type u_2<VAR>M : Type u_4<VAR>v : ι → M<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<GOAL>LinearIndependent R v ↔ ∀ (l : ι →₀ R), (Finsupp.total ι M R v) l = 0 → l = 0
<VAR>ι : Type u'<VAR>R : Type u_2<VAR>M : Type u_4<VAR>v : ι → M<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<GOAL>LinearIndependent R v ↔ ∀ (s : Finset ι) (g : ι → R), ∑ i ∈ s, g i • v i = 0 → ∀ i ∈ s, g i = 0
<VAR>ι : Type u'<VAR>R : Type u_2<VAR>M : Type u_4<VAR>v : ι → M<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<GOAL>LinearIndependent R v ↔ ∀ (s : Finset ι) (g : ι → R), (∀ i ∉ s, g i = 0) → ∑ i ∈ s, g i • v i = 0 → ∀ (i : ι), g i = 0
<VAR>ι : Type u'<VAR>R : Type u_2<VAR>M : Type u_4<VAR>v : ι → M<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<GOAL>¬LinearIndependent R v ↔ ∃ s g, ∑ i ∈ s, g i • v i = 0 ∧ ∃ i ∈ s, g i ≠ 0
<VAR>ι : Type u'<VAR>R : Type u_2<VAR>M : Type u_4<VAR>v : ι → M<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>Fintype ι<GOAL>LinearIndependent R v ↔ ∀ (g : ι → R), ∑ i : ι, g i • v i = 0 → ∀ (i : ι), g i = 0
<VAR>ι : Type u'<VAR>R : Type u_2<VAR>M : Type u_4<VAR>v : ι → M<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>Fintype ι<VAR>DecidableEq ι<GOAL>LinearIndependent R v ↔ LinearMap.ker ((LinearMap.lsum R (fun x => R) ℕ) fun i => LinearMap.id.smulRight (v i)) = ⊥
<VAR>ι : Type u'<VAR>R : Type u_2<VAR>M : Type u_4<VAR>v : ι → M<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>Fintype ι<GOAL>¬LinearIndependent R v ↔ ∃ g, ∑ i : ι, g i • v i = 0 ∧ ∃ i, g i ≠ 0
<VAR>ι : Type u'<VAR>R : Type u_2<VAR>M : Type u_4<VAR>v : ι → M<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>IsEmpty ι<GOAL>LinearIndependent R v
<VAR>ι : Type u'<VAR>R : Type u_2<VAR>M : Type u_4<VAR>v : ι → M<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>Nontrivial R<VAR>i : ι<VAR>hv : LinearIndependent R v<GOAL>v i ≠ 0
<VAR>R : Type u_2<VAR>M : Type u_4<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>x y : M<VAR>h : LinearIndependent R ![x, y]<VAR>s t : R<VAR>h' : s • x + t • y = 0<GOAL>s = 0 ∧ t = 0
<VAR>R : Type u_2<VAR>M : Type u_4<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>x y : M<GOAL>LinearIndependent R ![x, y] ↔ ∀ (s t : R), s • x + t • y = 0 → s = 0 ∧ t = 0
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R : Type u_2<VAR>M : Type u_4<VAR>v : ι → M<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>h : LinearIndependent R v<VAR>f : ι' → ι<VAR>hf : Function.Injective f<GOAL>LinearIndependent R (v ∘ f)
<VAR>ι : Type u'<VAR>R : Type u_2<VAR>M : Type u_4<VAR>v : ι → M<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<GOAL>LinearIndependent R v ↔ ∀ (s : Finset ι), LinearIndependent R (v ∘ Subtype.val)
<VAR>ι : Type u'<VAR>R : Type u_2<VAR>M : Type u_4<VAR>v : ι → M<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>i : LinearIndependent R v<GOAL>LinearIndependent (ι := { x // x ∈ Set.range v }) R Subtype.val
<VAR>ι : Type u'<VAR>R : Type u_2<VAR>M : Type u_4<VAR>M' : Type u_5<VAR>v : ι → M<VAR>Semiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid M'<VAR>Module R M<VAR>Module R M'<VAR>hv : LinearIndependent R v<VAR>f : M →ₗ[R] M'<VAR>hf_inj : Disjoint (Submodule.span R (Set.range v)) (LinearMap.ker f)<GOAL>LinearIndependent R (⇑f ∘ v)
<VAR>ι : Type u'<VAR>R : Type u_2<VAR>M : Type u_4<VAR>M' : Type u_5<VAR>v : ι → M<VAR>Semiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid M'<VAR>Module R M<VAR>Module R M'<VAR>f : M →ₗ[R] M'<VAR>hv : LinearIndependent R (⇑f ∘ v)<GOAL>Disjoint (Submodule.span R (Set.range v)) (LinearMap.ker f)
<VAR>ι : Type u'<VAR>R : Type u_2<VAR>M : Type u_4<VAR>M' : Type u_5<VAR>v : ι → M<VAR>Semiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid M'<VAR>Module R M<VAR>Module R M'<VAR>hv : LinearIndependent R v<VAR>f : M →ₗ[R] M'<VAR>hf_inj : LinearMap.ker f = ⊥<GOAL>LinearIndependent R (⇑f ∘ v)
<VAR>ι : Type u'<VAR>R : Type u_2<VAR>M : Type u_4<VAR>v : ι → M<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>R' : Type u_8<VAR>M' : Type u_9<VAR>Semiring R'<VAR>AddCommMonoid M'<VAR>Module R' M'<VAR>hv : LinearIndependent R v<VAR>i : R' → R<VAR>j : M →+ M'<VAR>hi : ∀ (r : R'), i r = 0 → r = 0<VAR>hj : ∀ (m : M), j m = 0 → m = 0<VAR>hc : ∀ (r : R') (m : M), j (i r • m) = r • j m<GOAL>LinearIndependent R' (⇑j ∘ v)
<VAR>ι : Type u'<VAR>R : Type u_2<VAR>M : Type u_4<VAR>v : ι → M<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>R' : Type u_8<VAR>M' : Type u_9<VAR>Semiring R'<VAR>AddCommMonoid M'<VAR>Module R' M'<VAR>hv : LinearIndependent R v<VAR>i : ZeroHom R R'<VAR>j : M →+ M'<VAR>hi : Function.Surjective ⇑i<VAR>hj : ∀ (m : M), j m = 0 → m = 0<VAR>hc : ∀ (r : R) (m : M), j (r • m) = i r • j m<GOAL>LinearIndependent R' (⇑j ∘ v)
<VAR>ι : Type u'<VAR>R : Type u_2<VAR>M : Type u_4<VAR>M' : Type u_5<VAR>v : ι → M<VAR>Semiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid M'<VAR>Module R M<VAR>Module R M'<VAR>f : M →ₗ[R] M'<VAR>hfv : LinearIndependent R (⇑f ∘ v)<GOAL>LinearIndependent R v
<VAR>ι : Type u'<VAR>R : Type u_2<VAR>M : Type u_4<VAR>M' : Type u_5<VAR>v : ι → M<VAR>Semiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid M'<VAR>Module R M<VAR>Module R M'<VAR>f : M →ₗ[R] M'<VAR>hf_inj : LinearMap.ker f = ⊥<GOAL>LinearIndependent R (⇑f ∘ v) ↔ LinearIndependent R v
<VAR>ι : Type u'<VAR>R : Type u_2<VAR>M : Type u_4<VAR>v : ι → M<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>Subsingleton R<GOAL>LinearIndependent R v
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R : Type u_2<VAR>M : Type u_4<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>e : ι ≃ ι'<VAR>f : ι' → M<GOAL>LinearIndependent R (f ∘ ⇑e) ↔ LinearIndependent R f
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R : Type u_2<VAR>M : Type u_4<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>e : ι ≃ ι'<VAR>f : ι' → M<VAR>g : ι → M<VAR>h : f ∘ ⇑e = g<GOAL>LinearIndependent R g ↔ LinearIndependent R f
<VAR>R : Type u_2<VAR>M : Type u_4<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>ι : Type u_8<VAR>f : ι → M<VAR>hf : Function.Injective f<GOAL>LinearIndependent (ι := { x // x ∈ Set.range f }) R Subtype.val ↔ LinearIndependent R f
<VAR>R : Type u_2<VAR>M : Type u_4<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>ι : Type u_8<VAR>s : Set ι<VAR>f : ι → M<VAR>hf : Set.InjOn f s<GOAL>(LinearIndependent R fun (x : ↑s) => f ↑x) ↔ LinearIndependent R fun (x : ↑(f '' s)) => ↑x
<VAR>ι : Type u'<VAR>R : Type u_2<VAR>M : Type u_4<VAR>v : ι → M<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>hs : LinearIndependent R v<GOAL>LinearIndependent R fun i => ⟨v i, ⋯⟩
<VAR>R : Type u_2<VAR>M : Type u_4<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>m : ℕ<VAR>x : M<VAR>v : Fin m → M<VAR>hli : LinearIndependent R v<VAR>x_ortho : ∀ (c : R) (y : ↥(Submodule.span R (Set.range v))), c • x + ↑y = 0 → c = 0<GOAL>LinearIndependent R (Fin.cons x v)
<VAR>ι : Type u'<VAR>R : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>v : ι → M<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>Semiring K<VAR>SMulWithZero R K<VAR>Module K M<VAR>IsScalarTower R K M<VAR>hinj : Function.Injective fun r => r • 1<VAR>li : LinearIndependent K v<GOAL>LinearIndependent R v
<VAR>R : Type u_2<VAR>M : Type u_4<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>s : Set M<VAR>li : LinearIndependent (ι := { x // x ∈ s }) R Subtype.val<VAR>t : Finset ↑s<GOAL>LinearIndependent R Subtype.val
<VAR>R : Type u_2<VAR>M : Type u_4<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>n : ℕ<VAR>H : ∀ (s : Finset M), (LinearIndependent R fun i => ↑i) → s.card ≤ n<VAR>s : Set M<GOAL>LinearIndependent (ι := { x // x ∈ s }) R Subtype.val → #↑s ≤ ↑n
<VAR>ι : Type u'<VAR>R : Type u_2<VAR>M : Type u_4<VAR>v : ι → M<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>s : Set ι<GOAL>LinearIndependent (ι := ↑s) R (v ∘ Subtype.val) ↔ ∀ l ∈ Finsupp.supported R R s, (Finsupp.total ι M R v) l = 0 → l = 0
<VAR>ι : Type u'<VAR>R : Type u_2<VAR>M : Type u_4<VAR>v : ι → M<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>s : Set ι<GOAL>¬LinearIndependent (ι := ↑s) R (v ∘ Subtype.val) ↔ ∃ f ∈ Finsupp.supported R R s, (Finsupp.total ι M R v) f = 0 ∧ f ≠ 0
<VAR>ι : Type u'<VAR>R : Type u_2<VAR>M : Type u_4<VAR>v : ι → M<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>s : Set ι<GOAL>¬LinearIndependent (ι := ↑s) R (v ∘ Subtype.val) ↔ ∃ f ∈ Finsupp.supported R R s, ∑ i ∈ f.support, f i • v i = 0 ∧ f ≠ 0
<VAR>R : Type u_2<VAR>M : Type u_4<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>s : Set M<GOAL>(LinearIndependent R fun (x : ↑s) => ↑x) ↔ ∀ l ∈ Finsupp.supported R R s, (Finsupp.total M M R id) l = 0 → l = 0
<VAR>ι : Type u'<VAR>R : Type u_2<VAR>M : Type u_4<VAR>v : ι → M<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>s : Set ι<GOAL>LinearIndependent (ι := ↑s) R (v ∘ Subtype.val) ↔ Disjoint (Finsupp.supported R R s) (LinearMap.ker (Finsupp.total ι M R v))
<VAR>R : Type u_2<VAR>M : Type u_4<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>s : Set M<GOAL>(LinearIndependent R fun (x : ↑s) => ↑x) ↔ Disjoint (Finsupp.supported R R s) (LinearMap.ker (Finsupp.total M M R id))
<VAR>R : Type u_2<VAR>M : Type u_4<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>s : Set M<GOAL>(LinearIndependent R fun (x : ↑s) => ↑x) ↔ LinearMap.ker (Finsupp.totalOn M M R id s) = ⊥
<VAR>ι : Type u'<VAR>R : Type u_2<VAR>M : Type u_4<VAR>v : ι → M<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>s : Set ι<VAR>hs : LinearIndependent (ι := ↑s) R (v ∘ Subtype.val)<GOAL>LinearIndependent (ι := ↑s) R (s.restrict v)
<VAR>R : Type u_2<VAR>M : Type u_4<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<GOAL>LinearIndependent R fun (x : ↑∅) => ↑x
<VAR>R : Type u_2<VAR>M : Type u_4<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>t s : Set M<VAR>h : t ⊆ s<GOAL>(LinearIndependent R fun (x : ↑s) => ↑x) → LinearIndependent R fun (x : ↑t) => ↑x