ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u<VAR>CommRing R<VAR>n : Type v<VAR>DecidableEq n<VAR>Fintype n<VAR>M : Matrix n n R<GOAL>IsIntegral R M
<VAR>n : Type v<VAR>DecidableEq n<VAR>Fintype n<VAR>K : Type u_1<VAR>Field K<VAR>M : Matrix n n K<GOAL>minpoly K M ∣ M.charpoly
<VAR>R : Type u<VAR>CommRing R<VAR>n : Type v<VAR>DecidableEq n<VAR>Fintype n<VAR>f : (n → R) →ₗ[R] n → R<GOAL>minpoly R (LinearMap.toMatrix' f) = minpoly R f
<VAR>R : Type u<VAR>CommRing R<VAR>n : Type v<VAR>DecidableEq n<VAR>Fintype n<VAR>N : Type w<VAR>AddCommGroup N<VAR>Module R N<VAR>b : Basis n R N<VAR>f : N →ₗ[R] N<GOAL>minpoly R ((LinearMap.toMatrix b b) f) = minpoly R f
<VAR>R : Type u<VAR>CommRing R<VAR>S : Type u_1<VAR>Ring S<VAR>Algebra R S<VAR>h : PowerBasis R S<GOAL>((Algebra.leftMulMatrix h.basis) h.gen).charpoly = minpoly R h.gen
<VAR>n : Type u_1<VAR>Fintype n<VAR>DecidableEq n<VAR>R : Type u_2<VAR>Field R<VAR>A : Matrix n n R<VAR>hAps : Polynomial.Splits (RingHom.id R) A.charpoly<GOAL>A.det = A.charpoly.roots.prod
<VAR>n : Type u_1<VAR>Fintype n<VAR>DecidableEq n<VAR>R : Type u_2<VAR>Field R<VAR>A : Matrix n n R<VAR>hAps : Polynomial.Splits (RingHom.id R) A.charpoly<GOAL>A.trace = A.charpoly.roots.sum
<VAR>n : Type u_1<VAR>Fintype n<VAR>DecidableEq n<VAR>R : Type u_2<VAR>Field R<VAR>A : Matrix n n R<VAR>IsAlgClosed R<GOAL>A.det = A.charpoly.roots.prod
<VAR>n : Type u_1<VAR>Fintype n<VAR>DecidableEq n<VAR>R : Type u_2<VAR>Field R<VAR>A : Matrix n n R<VAR>IsAlgClosed R<GOAL>A.trace = A.charpoly.roots.sum
<VAR>R : Type u_1<VAR>CommRing R<VAR>n : Type u_4<VAR>DecidableEq n<VAR>Fintype n<VAR>M : Matrix n n R<VAR>i j : n<GOAL>M.charmatrix i j = Matrix.diagonal (fun x => Polynomial.X) i j - Polynomial.C (M i j)
<VAR>R : Type u_1<VAR>CommRing R<VAR>n : Type u_4<VAR>DecidableEq n<VAR>Fintype n<VAR>M : Matrix n n R<VAR>i : n<GOAL>M.charmatrix i i = Polynomial.X - Polynomial.C (M i i)
<VAR>R : Type u_1<VAR>CommRing R<VAR>n : Type u_4<VAR>DecidableEq n<VAR>Fintype n<VAR>M : Matrix n n R<VAR>i j : n<VAR>h : i ≠ j<GOAL>M.charmatrix i j = -Polynomial.C (M i j)
<VAR>R : Type u_1<VAR>CommRing R<VAR>n : Type u_4<VAR>DecidableEq n<VAR>Fintype n<VAR>M : Matrix n n R<GOAL>matPolyEquiv M.charmatrix = Polynomial.X - Polynomial.C M
<VAR>R : Type u_1<VAR>CommRing R<VAR>m : Type u_3<VAR>n : Type u_4<VAR>DecidableEq m<VAR>DecidableEq n<VAR>Fintype m<VAR>Fintype n<VAR>M : Matrix n n R<VAR>e : n ≃ m<GOAL>((Matrix.reindex e e) M).charmatrix = (Matrix.reindex e e) M.charmatrix
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>CommRing R<VAR>CommRing S<VAR>n : Type u_4<VAR>DecidableEq n<VAR>Fintype n<VAR>M : Matrix n n R<VAR>f : R →+* S<GOAL>(M.map ⇑f).charmatrix = M.charmatrix.map (Polynomial.map f)
<VAR>R : Type u_1<VAR>CommRing R<VAR>m : Type u_3<VAR>n : Type u_4<VAR>DecidableEq m<VAR>DecidableEq n<VAR>Fintype m<VAR>Fintype n<VAR>M₁₁ : Matrix m m R<VAR>M₁₂ : Matrix m n R<VAR>M₂₁ : Matrix n m R<VAR>M₂₂ : Matrix n n R<GOAL>(Matrix.fromBlocks M₁₁ M₁₂ M₂₁ M₂₂).charmatrix = Matrix.fromBlocks M₁₁.charmatrix (-M₁₂.map ⇑Polynomial.C) (-M₂₁.map ⇑Polynomial.C) M₂₂.charmatrix
<VAR>R : Type u_1<VAR>CommRing R<VAR>m : Type u_3<VAR>n : Type u_4<VAR>DecidableEq m<VAR>DecidableEq n<VAR>Fintype m<VAR>Fintype n<VAR>e : n ≃ m<VAR>M : Matrix n n R<GOAL>((Matrix.reindex e e) M).charpoly = M.charpoly
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>CommRing R<VAR>CommRing S<VAR>n : Type u_4<VAR>DecidableEq n<VAR>Fintype n<VAR>M : Matrix n n R<VAR>f : R →+* S<GOAL>(M.map ⇑f).charpoly = Polynomial.map f M.charpoly
<VAR>R : Type u_1<VAR>CommRing R<VAR>m : Type u_3<VAR>n : Type u_4<VAR>DecidableEq m<VAR>DecidableEq n<VAR>Fintype m<VAR>Fintype n<VAR>M₁₁ : Matrix m m R<VAR>M₂₁ : Matrix n m R<VAR>M₂₂ : Matrix n n R<GOAL>(Matrix.fromBlocks M₁₁ 0 M₂₁ M₂₂).charpoly = M₁₁.charpoly * M₂₂.charpoly
<VAR>R : Type u_1<VAR>CommRing R<VAR>m : Type u_3<VAR>n : Type u_4<VAR>DecidableEq m<VAR>DecidableEq n<VAR>Fintype m<VAR>Fintype n<VAR>M₁₁ : Matrix m m R<VAR>M₁₂ : Matrix m n R<VAR>M₂₂ : Matrix n n R<GOAL>(Matrix.fromBlocks M₁₁ M₁₂ 0 M₂₂).charpoly = M₁₁.charpoly * M₂₂.charpoly
<VAR>R : Type u_1<VAR>CommRing R<VAR>n : Type u_4<VAR>DecidableEq n<VAR>Fintype n<VAR>M : Matrix n n R<GOAL>(Polynomial.aeval M) M.charpoly = 0
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>n : Type u_3<VAR>CommRing R<VAR>CommRing S<VAR>Fintype n<VAR>DecidableEq n<VAR>f : R →+* S<VAR>M : n × n → S<GOAL>Polynomial.map (MvPolynomial.eval₂Hom f M) (Matrix.charpoly.univ R n) = (Matrix.of (Function.curry M)).charpoly
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>n : Type u_3<VAR>CommRing R<VAR>CommRing S<VAR>Fintype n<VAR>DecidableEq n<VAR>f : R →+* S<GOAL>Polynomial.map (MvPolynomial.map f) (Matrix.charpoly.univ R n) = Matrix.charpoly.univ S n
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>n : Type u_3<VAR>CommRing R<VAR>CommRing S<VAR>Fintype n<VAR>DecidableEq n<VAR>f : R →+* S<VAR>M : n × n → S<VAR>i : ℕ<GOAL>(MvPolynomial.eval₂Hom f M) ((Matrix.charpoly.univ R n).coeff i) = (Matrix.of (Function.curry M)).charpoly.coeff i
<VAR>R : Type u_1<VAR>n : Type u_3<VAR>CommRing R<VAR>Fintype n<VAR>DecidableEq n<GOAL>(Matrix.charpoly.univ R n).Monic
<VAR>R : Type u_1<VAR>n : Type u_3<VAR>CommRing R<VAR>Fintype n<VAR>DecidableEq n<VAR>Nontrivial R<GOAL>(Matrix.charpoly.univ R n).natDegree = Fintype.card n
<VAR>R : Type u_1<VAR>n : Type u_3<VAR>CommRing R<VAR>Fintype n<VAR>DecidableEq n<GOAL>(Matrix.charpoly.univ R n).coeff (Fintype.card n) = 1
<VAR>R : Type u_1<VAR>n : Type u_3<VAR>CommRing R<VAR>Fintype n<VAR>DecidableEq n<GOAL>((MvPolynomial.optionEquivLeft R (n × n)).symm (Matrix.charpoly.univ R n)).IsHomogeneous (Fintype.card n)
<VAR>R : Type u_1<VAR>n : Type u_3<VAR>CommRing R<VAR>Fintype n<VAR>DecidableEq n<VAR>i j : ℕ<VAR>h : i + j = Fintype.card n<GOAL>((Matrix.charpoly.univ R n).coeff i).IsHomogeneous j
<VAR>n : Type u_1<VAR>DecidableEq n<VAR>Fintype n<VAR>K : Type u_2<VAR>Field K<VAR>Fintype K<VAR>M : Matrix n n K<GOAL>(M ^ Fintype.card K).charpoly = M.charpoly
<VAR>n : Type u_1<VAR>DecidableEq n<VAR>Fintype n<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>M : Matrix n n (ZMod p)<GOAL>(M ^ p).charpoly = M.charpoly
<VAR>n : Type u_1<VAR>DecidableEq n<VAR>Fintype n<VAR>K : Type u_2<VAR>Field K<VAR>Fintype K<VAR>M : Matrix n n K<GOAL>(M ^ Fintype.card K).trace = M.trace ^ Fintype.card K
<VAR>n : Type u_1<VAR>DecidableEq n<VAR>Fintype n<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>M : Matrix n n (ZMod p)<GOAL>(M ^ p).trace = M.trace ^ p
<VAR>𝕜 : Type u_1<VAR>RCLike 𝕜<VAR>n : Type u_2<VAR>Fintype n<VAR>A : Matrix n n 𝕜<VAR>DecidableEq n<VAR>hA : A.IsHermitian<VAR>j : n<GOAL>A.mulVec ((WithLp.equiv 2 ((i : n) → (fun x => 𝕜) i)) (hA.eigenvectorBasis j)) = hA.eigenvalues j • (WithLp.equiv 2 ((i : n) → (fun x => 𝕜) i)) (hA.eigenvectorBasis j)
<VAR>𝕜 : Type u_1<VAR>RCLike 𝕜<VAR>n : Type u_2<VAR>Fintype n<VAR>A : Matrix n n 𝕜<VAR>DecidableEq n<GOAL>spectrum 𝕜 (Matrix.toEuclideanLin A) = spectrum 𝕜 A
<VAR>𝕜 : Type u_1<VAR>RCLike 𝕜<VAR>n : Type u_2<VAR>Fintype n<VAR>A : Matrix n n 𝕜<VAR>DecidableEq n<VAR>hA : A.IsHermitian<VAR>i : n<GOAL>hA.eigenvalues i ∈ spectrum ℝ A
<VAR>𝕜 : Type u_3<VAR>RCLike 𝕜<VAR>n : Type u_4<VAR>Fintype n<VAR>A : Matrix n n 𝕜<VAR>DecidableEq n<VAR>hA : A.IsHermitian<GOAL>↑hA.eigenvectorUnitary = (EuclideanSpace.basisFun n 𝕜).toBasis.toMatrix ⇑hA.eigenvectorBasis.toBasis
<VAR>𝕜 : Type u_1<VAR>RCLike 𝕜<VAR>n : Type u_2<VAR>Fintype n<VAR>A : Matrix n n 𝕜<VAR>DecidableEq n<VAR>hA : A.IsHermitian<VAR>i j : n<GOAL>↑hA.eigenvectorUnitary i j = (WithLp.equiv 2 ((i : n) → (fun x => 𝕜) i)) (hA.eigenvectorBasis j) i
<VAR>𝕜 : Type u_1<VAR>RCLike 𝕜<VAR>n : Type u_2<VAR>Fintype n<VAR>A : Matrix n n 𝕜<VAR>DecidableEq n<VAR>hA : A.IsHermitian<VAR>j : n<GOAL>(↑hA.eigenvectorUnitary).mulVec (Pi.single j 1) = (WithLp.equiv 2 ((i : n) → (fun x => 𝕜) i)) (hA.eigenvectorBasis j)
<VAR>𝕜 : Type u_1<VAR>RCLike 𝕜<VAR>n : Type u_2<VAR>Fintype n<VAR>A : Matrix n n 𝕜<VAR>DecidableEq n<VAR>hA : A.IsHermitian<VAR>j : n<GOAL>(star ↑hA.eigenvectorUnitary).mulVec ((WithLp.equiv 2 ((i : n) → (fun x => 𝕜) i)) (hA.eigenvectorBasis j)) = Pi.single j 1
<VAR>𝕜 : Type u_1<VAR>RCLike 𝕜<VAR>n : Type u_2<VAR>Fintype n<VAR>A : Matrix n n 𝕜<VAR>DecidableEq n<VAR>hA : A.IsHermitian<GOAL>star ↑hA.eigenvectorUnitary * A * ↑hA.eigenvectorUnitary = Matrix.diagonal (RCLike.ofReal ∘ hA.eigenvalues)
<VAR>𝕜 : Type u_1<VAR>RCLike 𝕜<VAR>n : Type u_2<VAR>Fintype n<VAR>A : Matrix n n 𝕜<VAR>DecidableEq n<VAR>hA : A.IsHermitian<GOAL>A = ↑hA.eigenvectorUnitary * Matrix.diagonal (RCLike.ofReal ∘ hA.eigenvalues) * star ↑hA.eigenvectorUnitary
<VAR>𝕜 : Type u_1<VAR>RCLike 𝕜<VAR>n : Type u_2<VAR>Fintype n<VAR>A : Matrix n n 𝕜<VAR>DecidableEq n<VAR>hA : A.IsHermitian<VAR>i : n<GOAL>hA.eigenvalues i = RCLike.re (Matrix.dotProduct (star ((WithLp.equiv 2 ((i : n) → (fun x => 𝕜) i)) (hA.eigenvectorBasis i))) (A.mulVec ((WithLp.equiv 2 ((i : n) → (fun x => 𝕜) i)) (hA.eigenvectorBasis i))))
<VAR>𝕜 : Type u_1<VAR>RCLike 𝕜<VAR>n : Type u_2<VAR>Fintype n<VAR>A : Matrix n n 𝕜<VAR>DecidableEq n<VAR>hA : A.IsHermitian<GOAL>A.det = ∏ i : n, ↑(hA.eigenvalues i)
<VAR>𝕜 : Type u_1<VAR>RCLike 𝕜<VAR>n : Type u_2<VAR>Fintype n<VAR>A : Matrix n n 𝕜<VAR>DecidableEq n<VAR>hA : A.IsHermitian<GOAL>A.rank = (Matrix.diagonal hA.eigenvalues).rank
<VAR>𝕜 : Type u_1<VAR>RCLike 𝕜<VAR>n : Type u_2<VAR>Fintype n<VAR>A : Matrix n n 𝕜<VAR>DecidableEq n<VAR>hA : A.IsHermitian<GOAL>A.rank = Fintype.card { i // hA.eigenvalues i ≠ 0 }
<VAR>𝕜 : Type u_1<VAR>RCLike 𝕜<VAR>n : Type u_2<VAR>Fintype n<VAR>A : Matrix n n 𝕜<VAR>hA : A.IsHermitian<VAR>h_ne : A ≠ 0<GOAL>∃ v t, t ≠ 0 ∧ v ≠ 0 ∧ A.mulVec v = t • v
<VAR>m : Type u_1<VAR>R : Type u_2<VAR>Fintype m<VAR>CommRing R<VAR>M : Matrix m m R<VAR>hM : M.Nondegenerate<VAR>v : m → R<VAR>hv : ∀ (w : m → R), Matrix.dotProduct v (M.mulVec w) = 0<GOAL>v = 0
<VAR>m : Type u_1<VAR>R : Type u_2<VAR>Fintype m<VAR>CommRing R<VAR>M : Matrix m m R<VAR>hM : M.Nondegenerate<VAR>v : m → R<VAR>hv : v ≠ 0<GOAL>∃ w, Matrix.dotProduct v (M.mulVec w) ≠ 0
<VAR>m : Type u_1<VAR>A : Type u_3<VAR>Fintype m<VAR>CommRing A<VAR>IsDomain A<VAR>DecidableEq m<VAR>M : Matrix m m A<VAR>hM : M.det ≠ 0<GOAL>M.Nondegenerate
<VAR>m : Type u_1<VAR>A : Type u_3<VAR>Fintype m<VAR>CommRing A<VAR>IsDomain A<VAR>DecidableEq m<VAR>M : Matrix m m A<VAR>hM : M.det ≠ 0<VAR>v : m → A<VAR>hv : Matrix.vecMul v M = 0<GOAL>v = 0
<VAR>m : Type u_1<VAR>A : Type u_3<VAR>Fintype m<VAR>CommRing A<VAR>IsDomain A<VAR>DecidableEq m<VAR>M : Matrix m m A<VAR>hM : M.det ≠ 0<VAR>v : m → A<VAR>hv : M.mulVec v = 0<GOAL>v = 0
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>S : AffineSpace V P<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>w : ι → k<VAR>p : ι → P<VAR>b : P<GOAL>(s.weightedVSubOfPoint p b) w = ∑ i ∈ s, w i • (p i -ᵥ b)
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>S : AffineSpace V P<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>w : ι → k<VAR>p b : P<GOAL>(s.weightedVSubOfPoint (fun x => p) b) w = (∑ i ∈ s, w i) • (p -ᵥ b)
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>S : AffineSpace V P<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>w : ι → k<VAR>p : ι → P<VAR>b : P<VAR>v : V<GOAL>(s.weightedVSubOfPoint (v +ᵥ p) b) w = (s.weightedVSubOfPoint p (-v +ᵥ b)) w
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>S : AffineSpace V P<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>w₁ w₂ : ι → k<VAR>hw : ∀ i ∈ s, w₁ i = w₂ i<VAR>p₁ p₂ : ι → P<VAR>hp : ∀ i ∈ s, p₁ i = p₂ i<VAR>b : P<GOAL>(s.weightedVSubOfPoint p₁ b) w₁ = (s.weightedVSubOfPoint p₂ b) w₂
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>S : AffineSpace V P<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>p : ι → P<VAR>j : ι<VAR>w₁ w₂ : ι → k<VAR>hw : ∀ (i : ι), i ≠ j → w₁ i = w₂ i<GOAL>(s.weightedVSubOfPoint p (p j)) w₁ = (s.weightedVSubOfPoint p (p j)) w₂
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>S : AffineSpace V P<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>w : ι → k<VAR>p : ι → P<VAR>h : ∑ i ∈ s, w i = 0<VAR>b₁ b₂ : P<GOAL>(s.weightedVSubOfPoint p b₁) w = (s.weightedVSubOfPoint p b₂) w
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>S : AffineSpace V P<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>w : ι → k<VAR>p : ι → P<VAR>h : ∑ i ∈ s, w i = 1<VAR>b₁ b₂ : P<GOAL>(s.weightedVSubOfPoint p b₁) w +ᵥ b₁ = (s.weightedVSubOfPoint p b₂) w +ᵥ b₂
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>S : AffineSpace V P<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>DecidableEq ι<VAR>w : ι → k<VAR>p : ι → P<VAR>i : ι<GOAL>((s.erase i).weightedVSubOfPoint p (p i)) w = (s.weightedVSubOfPoint p (p i)) w
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>S : AffineSpace V P<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>DecidableEq ι<VAR>w : ι → k<VAR>p : ι → P<VAR>i : ι<GOAL>((insert i s).weightedVSubOfPoint p (p i)) w = (s.weightedVSubOfPoint p (p i)) w
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>S : AffineSpace V P<VAR>ι : Type u_4<VAR>w : ι → k<VAR>p : ι → P<VAR>b : P<VAR>s₁ s₂ : Finset ι<VAR>h : s₁ ⊆ s₂<GOAL>(s₁.weightedVSubOfPoint p b) w = (s₂.weightedVSubOfPoint p b) ((↑s₁).indicator w)
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>S : AffineSpace V P<VAR>ι : Type u_4<VAR>ι₂ : Type u_5<VAR>s₂ : Finset ι₂<VAR>e : ι₂ ↪ ι<VAR>w : ι → k<VAR>p : ι → P<VAR>b : P<GOAL>((Finset.map e s₂).weightedVSubOfPoint p b) w = (s₂.weightedVSubOfPoint (p ∘ ⇑e) b) (w ∘ ⇑e)
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>S : AffineSpace V P<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>w : ι → k<VAR>p₁ p₂ : ι → P<VAR>b : P<GOAL>∑ i ∈ s, w i • (p₁ i -ᵥ p₂ i) = (s.weightedVSubOfPoint p₁ b) w - (s.weightedVSubOfPoint p₂ b) w
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>S : AffineSpace V P<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>w : ι → k<VAR>p₁ : ι → P<VAR>p₂ b : P<GOAL>∑ i ∈ s, w i • (p₁ i -ᵥ p₂) = (s.weightedVSubOfPoint p₁ b) w - (∑ i ∈ s, w i) • (p₂ -ᵥ b)
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>S : AffineSpace V P<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>w : ι → k<VAR>p₂ : ι → P<VAR>p₁ b : P<GOAL>∑ i ∈ s, w i • (p₁ -ᵥ p₂ i) = (∑ i ∈ s, w i) • (p₁ -ᵥ b) - (s.weightedVSubOfPoint p₂ b) w
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>S : AffineSpace V P<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>DecidableEq ι<VAR>s₂ : Finset ι<VAR>h : s₂ ⊆ s<VAR>w : ι → k<VAR>p : ι → P<VAR>b : P<GOAL>((s \ s₂).weightedVSubOfPoint p b) w + (s₂.weightedVSubOfPoint p b) w = (s.weightedVSubOfPoint p b) w
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>S : AffineSpace V P<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>DecidableEq ι<VAR>s₂ : Finset ι<VAR>h : s₂ ⊆ s<VAR>w : ι → k<VAR>p : ι → P<VAR>b : P<GOAL>((s \ s₂).weightedVSubOfPoint p b) w - (s₂.weightedVSubOfPoint p b) (-w) = (s.weightedVSubOfPoint p b) w
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>S : AffineSpace V P<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>w : ι → k<VAR>p : ι → P<VAR>b : P<VAR>pred : ι → Prop<VAR>DecidablePred pred<GOAL>(((Finset.subtype pred s).weightedVSubOfPoint (fun i => p ↑i) b) fun i => w ↑i) = ((Finset.filter pred s).weightedVSubOfPoint p b) w
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>S : AffineSpace V P<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>w : ι → k<VAR>p : ι → P<VAR>b : P<VAR>pred : ι → Prop<VAR>DecidablePred pred<VAR>h : ∀ i ∈ s, w i ≠ 0 → pred i<GOAL>((Finset.filter pred s).weightedVSubOfPoint p b) w = (s.weightedVSubOfPoint p b) w
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>S : AffineSpace V P<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>w : ι → k<VAR>p : ι → P<VAR>b : P<VAR>c : k<GOAL>(s.weightedVSubOfPoint p b) (c • w) = c • (s.weightedVSubOfPoint p b) w
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>S : AffineSpace V P<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>w : ι → k<VAR>p : ι → P<GOAL>(s.weightedVSub p) w = ∑ i ∈ s, w i • (p i -ᵥ Classical.choice ⋯)
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>S : AffineSpace V P<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>w : ι → k<VAR>p : ι → P<VAR>h : ∑ i ∈ s, w i = 0<VAR>b : P<GOAL>(s.weightedVSub p) w = (s.weightedVSubOfPoint p b) w
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>S : AffineSpace V P<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>w : ι → k<VAR>p : P<VAR>h : ∑ i ∈ s, w i = 0<GOAL>(s.weightedVSub fun x => p) w = 0
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>S : AffineSpace V P<VAR>ι : Type u_4<VAR>w : ι → k<VAR>p : ι → P<GOAL>(∅.weightedVSub p) w = 0
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>S : AffineSpace V P<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>w : ι → k<VAR>h : ∑ i ∈ s, w i = 0<VAR>p : ι → P<VAR>v : V<GOAL>(s.weightedVSub (v +ᵥ p)) w = (s.weightedVSub p) w
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>S : AffineSpace V P<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>w₁ w₂ : ι → k<VAR>hw : ∀ i ∈ s, w₁ i = w₂ i<VAR>p₁ p₂ : ι → P<VAR>hp : ∀ i ∈ s, p₁ i = p₂ i<GOAL>(s.weightedVSub p₁) w₁ = (s.weightedVSub p₂) w₂
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>S : AffineSpace V P<VAR>ι : Type u_4<VAR>w : ι → k<VAR>p : ι → P<VAR>s₁ s₂ : Finset ι<VAR>h : s₁ ⊆ s₂<GOAL>(s₁.weightedVSub p) w = (s₂.weightedVSub p) ((↑s₁).indicator w)
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>S : AffineSpace V P<VAR>ι : Type u_4<VAR>ι₂ : Type u_5<VAR>s₂ : Finset ι₂<VAR>e : ι₂ ↪ ι<VAR>w : ι → k<VAR>p : ι → P<GOAL>((Finset.map e s₂).weightedVSub p) w = (s₂.weightedVSub (p ∘ ⇑e)) (w ∘ ⇑e)
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>S : AffineSpace V P<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>w : ι → k<VAR>p₁ p₂ : ι → P<GOAL>∑ i ∈ s, w i • (p₁ i -ᵥ p₂ i) = (s.weightedVSub p₁) w - (s.weightedVSub p₂) w
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>S : AffineSpace V P<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>w : ι → k<VAR>p₁ : ι → P<VAR>p₂ : P<VAR>h : ∑ i ∈ s, w i = 0<GOAL>∑ i ∈ s, w i • (p₁ i -ᵥ p₂) = (s.weightedVSub p₁) w
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>S : AffineSpace V P<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>w : ι → k<VAR>p₂ : ι → P<VAR>p₁ : P<VAR>h : ∑ i ∈ s, w i = 0<GOAL>∑ i ∈ s, w i • (p₁ -ᵥ p₂ i) = -(s.weightedVSub p₂) w
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>S : AffineSpace V P<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>DecidableEq ι<VAR>s₂ : Finset ι<VAR>h : s₂ ⊆ s<VAR>w : ι → k<VAR>p : ι → P<GOAL>((s \ s₂).weightedVSub p) w + (s₂.weightedVSub p) w = (s.weightedVSub p) w
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>S : AffineSpace V P<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>DecidableEq ι<VAR>s₂ : Finset ι<VAR>h : s₂ ⊆ s<VAR>w : ι → k<VAR>p : ι → P<GOAL>((s \ s₂).weightedVSub p) w - (s₂.weightedVSub p) (-w) = (s.weightedVSub p) w
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>S : AffineSpace V P<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>w : ι → k<VAR>p : ι → P<VAR>pred : ι → Prop<VAR>DecidablePred pred<GOAL>(((Finset.subtype pred s).weightedVSub fun i => p ↑i) fun i => w ↑i) = ((Finset.filter pred s).weightedVSub p) w
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>S : AffineSpace V P<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>w : ι → k<VAR>p : ι → P<VAR>pred : ι → Prop<VAR>DecidablePred pred<VAR>h : ∀ i ∈ s, w i ≠ 0 → pred i<GOAL>((Finset.filter pred s).weightedVSub p) w = (s.weightedVSub p) w
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>S : AffineSpace V P<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>w : ι → k<VAR>p : ι → P<VAR>c : k<GOAL>(s.weightedVSub p) (c • w) = c • (s.weightedVSub p) w
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>S : AffineSpace V P<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>p : ι → P<GOAL>(Finset.affineCombination k s p).linear = s.weightedVSub p
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>S : AffineSpace V P<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>w : ι → k<VAR>p : ι → P<GOAL>(Finset.affineCombination k s p) w = (s.weightedVSubOfPoint p (Classical.choice ⋯)) w +ᵥ Classical.choice ⋯
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>S : AffineSpace V P<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>w : ι → k<VAR>p : P<VAR>h : ∑ i ∈ s, w i = 1<GOAL>(Finset.affineCombination k s fun x => p) w = p
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>S : AffineSpace V P<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>w₁ w₂ : ι → k<VAR>hw : ∀ i ∈ s, w₁ i = w₂ i<VAR>p₁ p₂ : ι → P<VAR>hp : ∀ i ∈ s, p₁ i = p₂ i<GOAL>(Finset.affineCombination k s p₁) w₁ = (Finset.affineCombination k s p₂) w₂
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>S : AffineSpace V P<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>w : ι → k<VAR>p : ι → P<VAR>h : ∑ i ∈ s, w i = 1<VAR>b : P<GOAL>(Finset.affineCombination k s p) w = (s.weightedVSubOfPoint p b) w +ᵥ b
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>S : AffineSpace V P<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>w₁ w₂ : ι → k<VAR>p : ι → P<GOAL>(s.weightedVSub p) w₁ +ᵥ (Finset.affineCombination k s p) w₂ = (Finset.affineCombination k s p) (w₁ + w₂)
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>S : AffineSpace V P<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>w₁ w₂ : ι → k<VAR>p : ι → P<GOAL>(Finset.affineCombination k s p) w₁ -ᵥ (Finset.affineCombination k s p) w₂ = (s.weightedVSub p) (w₁ - w₂)
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>S : AffineSpace V P<VAR>DecidableEq P<VAR>s : Finset P<VAR>w : P → k<VAR>f : { x // x ∈ s } → P<VAR>hf : Function.Injective f<GOAL>(Finset.affineCombination k s.attach f) (w ∘ f) = (Finset.affineCombination k (Finset.image f Finset.univ) id) w
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>S : AffineSpace V P<VAR>s : Finset P<VAR>w : P → k<GOAL>(Finset.affineCombination k s.attach Subtype.val) (w ∘ Subtype.val) = (Finset.affineCombination k s id) w
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>ι : Type u_6<VAR>s : Finset ι<VAR>w : ι → k<VAR>p : ι → V<VAR>hw : s.sum w = 0<GOAL>(s.weightedVSub p) w = ∑ i ∈ s, w i • p i
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>p : ι → V<VAR>w : ι → k<VAR>hw : ∑ i ∈ s, w i = 1<GOAL>(Finset.affineCombination k s p) w = ∑ i ∈ s, w i • p i
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>S : AffineSpace V P<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>w : ι → k<VAR>p : ι → P<VAR>i : ι<VAR>his : i ∈ s<VAR>hwi : w i = 1<VAR>hw0 : ∀ i2 ∈ s, i2 ≠ i → w i2 = 0<GOAL>(Finset.affineCombination k s p) w = p i
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>S : AffineSpace V P<VAR>ι : Type u_4<VAR>w : ι → k<VAR>p : ι → P<VAR>s₁ s₂ : Finset ι<VAR>h : s₁ ⊆ s₂<GOAL>(Finset.affineCombination k s₁ p) w = (Finset.affineCombination k s₂ p) ((↑s₁).indicator w)