ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R₂ : Type u_5<VAR>CommSemiring R₂<VAR>n : Type u_11<VAR>Fintype n<VAR>DecidableEq n<VAR>B : LinearMap.BilinForm R₂ (n → R₂)<VAR>M : Matrix n n R₂<GOAL>M * LinearMap.BilinForm.toMatrix' B = LinearMap.BilinForm.toMatrix' (B.compLeft (Matrix.toLin' M.transpose))
<VAR>R₂ : Type u_5<VAR>CommSemiring R₂<VAR>n : Type u_11<VAR>Fintype n<VAR>DecidableEq n<VAR>B : LinearMap.BilinForm R₂ (n → R₂)<VAR>M : Matrix n n R₂<GOAL>LinearMap.BilinForm.toMatrix' B * M = LinearMap.BilinForm.toMatrix' (B.compRight (Matrix.toLin' M))
<VAR>R₂ : Type u_5<VAR>CommSemiring R₂<VAR>n : Type u_11<VAR>o : Type u_12<VAR>Fintype n<VAR>Fintype o<VAR>DecidableEq n<VAR>DecidableEq o<VAR>M : Matrix n n R₂<VAR>P Q : Matrix n o R₂<GOAL>(Matrix.toBilin' M).comp (Matrix.toLin' P) (Matrix.toLin' Q) = Matrix.toBilin' (P.transpose * M * Q)
<VAR>R₂ : Type u_5<VAR>M₂ : Type u_6<VAR>CommSemiring R₂<VAR>AddCommMonoid M₂<VAR>Module R₂ M₂<VAR>n : Type u_11<VAR>Fintype n<VAR>DecidableEq n<VAR>b : Basis n R₂ M₂<VAR>B : LinearMap.BilinForm R₂ M₂<VAR>i j : n<GOAL>(BilinForm.toMatrix b) B i j = (B (b i)) (b j)
<VAR>R₂ : Type u_5<VAR>M₂ : Type u_6<VAR>CommSemiring R₂<VAR>AddCommMonoid M₂<VAR>Module R₂ M₂<VAR>n : Type u_11<VAR>Fintype n<VAR>DecidableEq n<VAR>b : Basis n R₂ M₂<VAR>M : Matrix n n R₂<VAR>x y : M₂<GOAL>(((Matrix.toBilin b) M) x) y = ∑ i : n, ∑ j : n, (b.repr x) i * M i j * (b.repr y) j
<VAR>R₂ : Type u_5<VAR>M₂ : Type u_6<VAR>CommSemiring R₂<VAR>AddCommMonoid M₂<VAR>Module R₂ M₂<VAR>n : Type u_11<VAR>Fintype n<VAR>DecidableEq n<VAR>b : Basis n R₂ M₂<VAR>B : LinearMap.BilinForm R₂ M₂<GOAL>(BilinForm.toMatrixAux ⇑b) B = (BilinForm.toMatrix b) B
<VAR>R₂ : Type u_5<VAR>M₂ : Type u_6<VAR>CommSemiring R₂<VAR>AddCommMonoid M₂<VAR>Module R₂ M₂<VAR>n : Type u_11<VAR>Fintype n<VAR>DecidableEq n<VAR>b : Basis n R₂ M₂<GOAL>(BilinForm.toMatrix b).symm = Matrix.toBilin b
<VAR>R₂ : Type u_5<VAR>M₂ : Type u_6<VAR>CommSemiring R₂<VAR>AddCommMonoid M₂<VAR>Module R₂ M₂<VAR>n : Type u_11<VAR>Fintype n<VAR>DecidableEq n<VAR>b : Basis n R₂ M₂<GOAL>(Matrix.toBilin b).symm = BilinForm.toMatrix b
<VAR>R₂ : Type u_5<VAR>CommSemiring R₂<VAR>n : Type u_11<VAR>Fintype n<VAR>DecidableEq n<GOAL>Matrix.toBilin (Pi.basisFun R₂ n) = Matrix.toBilin'
<VAR>R₂ : Type u_5<VAR>CommSemiring R₂<VAR>n : Type u_11<VAR>Fintype n<VAR>DecidableEq n<GOAL>BilinForm.toMatrix (Pi.basisFun R₂ n) = LinearMap.BilinForm.toMatrix'
<VAR>R₂ : Type u_5<VAR>M₂ : Type u_6<VAR>CommSemiring R₂<VAR>AddCommMonoid M₂<VAR>Module R₂ M₂<VAR>n : Type u_11<VAR>Fintype n<VAR>DecidableEq n<VAR>b : Basis n R₂ M₂<VAR>B : LinearMap.BilinForm R₂ M₂<GOAL>(Matrix.toBilin b) ((BilinForm.toMatrix b) B) = B
<VAR>R₂ : Type u_5<VAR>M₂ : Type u_6<VAR>CommSemiring R₂<VAR>AddCommMonoid M₂<VAR>Module R₂ M₂<VAR>n : Type u_11<VAR>Fintype n<VAR>DecidableEq n<VAR>b : Basis n R₂ M₂<VAR>M : Matrix n n R₂<GOAL>(BilinForm.toMatrix b) ((Matrix.toBilin b) M) = M
<VAR>R₂ : Type u_5<VAR>M₂ : Type u_6<VAR>CommSemiring R₂<VAR>AddCommMonoid M₂<VAR>Module R₂ M₂<VAR>n : Type u_11<VAR>o : Type u_12<VAR>Fintype n<VAR>Fintype o<VAR>DecidableEq n<VAR>b : Basis n R₂ M₂<VAR>M₂' : Type u_13<VAR>AddCommMonoid M₂'<VAR>Module R₂ M₂'<VAR>c : Basis o R₂ M₂'<VAR>DecidableEq o<VAR>B : LinearMap.BilinForm R₂ M₂<VAR>l r : M₂' →ₗ[R₂] M₂<GOAL>(BilinForm.toMatrix c) (B.comp l r) = ((LinearMap.toMatrix c b) l).transpose * (BilinForm.toMatrix b) B * (LinearMap.toMatrix c b) r
<VAR>R₂ : Type u_5<VAR>M₂ : Type u_6<VAR>CommSemiring R₂<VAR>AddCommMonoid M₂<VAR>Module R₂ M₂<VAR>n : Type u_11<VAR>Fintype n<VAR>DecidableEq n<VAR>b : Basis n R₂ M₂<VAR>B : LinearMap.BilinForm R₂ M₂<VAR>f : M₂ →ₗ[R₂] M₂<GOAL>(BilinForm.toMatrix b) (B.compLeft f) = ((LinearMap.toMatrix b b) f).transpose * (BilinForm.toMatrix b) B
<VAR>R₂ : Type u_5<VAR>M₂ : Type u_6<VAR>CommSemiring R₂<VAR>AddCommMonoid M₂<VAR>Module R₂ M₂<VAR>n : Type u_11<VAR>Fintype n<VAR>DecidableEq n<VAR>b : Basis n R₂ M₂<VAR>B : LinearMap.BilinForm R₂ M₂<VAR>f : M₂ →ₗ[R₂] M₂<GOAL>(BilinForm.toMatrix b) (B.compRight f) = (BilinForm.toMatrix b) B * (LinearMap.toMatrix b b) f
<VAR>R₂ : Type u_5<VAR>M₂ : Type u_6<VAR>CommSemiring R₂<VAR>AddCommMonoid M₂<VAR>Module R₂ M₂<VAR>n : Type u_11<VAR>o : Type u_12<VAR>Fintype n<VAR>Fintype o<VAR>DecidableEq n<VAR>b : Basis n R₂ M₂<VAR>DecidableEq o<VAR>c : Basis o R₂ M₂<VAR>B : LinearMap.BilinForm R₂ M₂<GOAL>(b.toMatrix ⇑c).transpose * (BilinForm.toMatrix b) B * b.toMatrix ⇑c = (BilinForm.toMatrix c) B
<VAR>R₂ : Type u_5<VAR>M₂ : Type u_6<VAR>CommSemiring R₂<VAR>AddCommMonoid M₂<VAR>Module R₂ M₂<VAR>n : Type u_11<VAR>o : Type u_12<VAR>Fintype n<VAR>Fintype o<VAR>DecidableEq n<VAR>b : Basis n R₂ M₂<VAR>M₂' : Type u_13<VAR>AddCommMonoid M₂'<VAR>Module R₂ M₂'<VAR>c : Basis o R₂ M₂'<VAR>DecidableEq o<VAR>B : LinearMap.BilinForm R₂ M₂<VAR>M : Matrix o n R₂<VAR>N : Matrix n o R₂<GOAL>M * (BilinForm.toMatrix b) B * N = (BilinForm.toMatrix c) (B.comp ((Matrix.toLin c b) M.transpose) ((Matrix.toLin c b) N))
<VAR>R₂ : Type u_5<VAR>M₂ : Type u_6<VAR>CommSemiring R₂<VAR>AddCommMonoid M₂<VAR>Module R₂ M₂<VAR>n : Type u_11<VAR>Fintype n<VAR>DecidableEq n<VAR>b : Basis n R₂ M₂<VAR>B : LinearMap.BilinForm R₂ M₂<VAR>M : Matrix n n R₂<GOAL>M * (BilinForm.toMatrix b) B = (BilinForm.toMatrix b) (B.compLeft ((Matrix.toLin b b) M.transpose))
<VAR>R₂ : Type u_5<VAR>M₂ : Type u_6<VAR>CommSemiring R₂<VAR>AddCommMonoid M₂<VAR>Module R₂ M₂<VAR>n : Type u_11<VAR>Fintype n<VAR>DecidableEq n<VAR>b : Basis n R₂ M₂<VAR>B : LinearMap.BilinForm R₂ M₂<VAR>M : Matrix n n R₂<GOAL>(BilinForm.toMatrix b) B * M = (BilinForm.toMatrix b) (B.compRight ((Matrix.toLin b b) M))
<VAR>R₂ : Type u_5<VAR>M₂ : Type u_6<VAR>CommSemiring R₂<VAR>AddCommMonoid M₂<VAR>Module R₂ M₂<VAR>n : Type u_11<VAR>o : Type u_12<VAR>Fintype n<VAR>Fintype o<VAR>DecidableEq n<VAR>b : Basis n R₂ M₂<VAR>M₂' : Type u_13<VAR>AddCommMonoid M₂'<VAR>Module R₂ M₂'<VAR>c : Basis o R₂ M₂'<VAR>DecidableEq o<VAR>M : Matrix n n R₂<VAR>P Q : Matrix n o R₂<GOAL>((Matrix.toBilin b) M).comp ((Matrix.toLin c b) P) ((Matrix.toLin c b) Q) = (Matrix.toBilin c) (P.transpose * M * Q)
<VAR>R₃ : Type u_7<VAR>CommRing R₃<VAR>n : Type u_11<VAR>Fintype n<VAR>J J₃ A A' : Matrix n n R₃<VAR>DecidableEq n<GOAL>(Matrix.toBilin' J).IsAdjointPair (Matrix.toBilin' J₃) (Matrix.toLin' A) (Matrix.toLin' A') ↔ J.IsAdjointPair J₃ A A'
<VAR>R₃ : Type u_7<VAR>M₃ : Type u_8<VAR>CommRing R₃<VAR>AddCommGroup M₃<VAR>Module R₃ M₃<VAR>n : Type u_11<VAR>Fintype n<VAR>b : Basis n R₃ M₃<VAR>J J₃ A A' : Matrix n n R₃<VAR>DecidableEq n<GOAL>((Matrix.toBilin b) J).IsAdjointPair ((Matrix.toBilin b) J₃) ((Matrix.toLin b b) A) ((Matrix.toLin b b) A') ↔ J.IsAdjointPair J₃ A A'
<VAR>R₃ : Type u_7<VAR>CommRing R₃<VAR>n : Type u_11<VAR>Fintype n<VAR>J A A' : Matrix n n R₃<VAR>DecidableEq n<VAR>P : Matrix n n R₃<VAR>h : IsUnit P<GOAL>(P.transpose * J * P).IsAdjointPair (P.transpose * J * P) A A' ↔ J.IsAdjointPair J (P * A * P⁻¹) (P * A' * P⁻¹)
<VAR>R₃ : Type u_7<VAR>CommRing R₃<VAR>n : Type u_11<VAR>Fintype n<VAR>J J₃ A : Matrix n n R₃<VAR>DecidableEq n<GOAL>A ∈ pairSelfAdjointMatricesSubmodule J J₃ ↔ J.IsAdjointPair J₃ A A
<VAR>R₃ : Type u_7<VAR>CommRing R₃<VAR>n : Type u_11<VAR>Fintype n<VAR>J A : Matrix n n R₃<VAR>DecidableEq n<GOAL>A ∈ selfAdjointMatricesSubmodule J ↔ J.IsSelfAdjoint A
<VAR>R₃ : Type u_7<VAR>CommRing R₃<VAR>n : Type u_11<VAR>Fintype n<VAR>J A : Matrix n n R₃<VAR>DecidableEq n<GOAL>A ∈ skewAdjointMatricesSubmodule J ↔ J.IsSkewAdjoint A
<VAR>R₂ : Type u_5<VAR>M₂ : Type u_6<VAR>CommSemiring R₂<VAR>AddCommMonoid M₂<VAR>Module R₂ M₂<VAR>ι : Type u_12<VAR>DecidableEq ι<VAR>Fintype ι<VAR>M : Matrix ι ι R₂<VAR>b : Basis ι R₂ M₂<GOAL>(Matrix.toBilin' M).Nondegenerate ↔ ((Matrix.toBilin b) M).Nondegenerate
<VAR>R₃ : Type u_7<VAR>CommRing R₃<VAR>ι : Type u_12<VAR>DecidableEq ι<VAR>Fintype ι<VAR>M : Matrix ι ι R₃<VAR>h : M.Nondegenerate<GOAL>(Matrix.toBilin' M).Nondegenerate
<VAR>R₃ : Type u_7<VAR>CommRing R₃<VAR>ι : Type u_12<VAR>DecidableEq ι<VAR>Fintype ι<VAR>M : Matrix ι ι R₃<GOAL>(Matrix.toBilin' M).Nondegenerate ↔ M.Nondegenerate
<VAR>R₃ : Type u_7<VAR>M₃ : Type u_8<VAR>CommRing R₃<VAR>AddCommGroup M₃<VAR>Module R₃ M₃<VAR>ι : Type u_12<VAR>DecidableEq ι<VAR>Fintype ι<VAR>M : Matrix ι ι R₃<VAR>h : M.Nondegenerate<VAR>b : Basis ι R₃ M₃<GOAL>((Matrix.toBilin b) M).Nondegenerate
<VAR>R₃ : Type u_7<VAR>M₃ : Type u_8<VAR>CommRing R₃<VAR>AddCommGroup M₃<VAR>Module R₃ M₃<VAR>ι : Type u_12<VAR>DecidableEq ι<VAR>Fintype ι<VAR>M : Matrix ι ι R₃<VAR>b : Basis ι R₃ M₃<GOAL>((Matrix.toBilin b) M).Nondegenerate ↔ M.Nondegenerate
<VAR>R₃ : Type u_7<VAR>CommRing R₃<VAR>ι : Type u_12<VAR>DecidableEq ι<VAR>Fintype ι<VAR>B : LinearMap.BilinForm R₃ (ι → R₃)<GOAL>(LinearMap.BilinForm.toMatrix' B).Nondegenerate ↔ B.Nondegenerate
<VAR>R₃ : Type u_7<VAR>CommRing R₃<VAR>ι : Type u_12<VAR>DecidableEq ι<VAR>Fintype ι<VAR>B : LinearMap.BilinForm R₃ (ι → R₃)<VAR>h : B.Nondegenerate<GOAL>(LinearMap.BilinForm.toMatrix' B).Nondegenerate
<VAR>R₃ : Type u_7<VAR>M₃ : Type u_8<VAR>CommRing R₃<VAR>AddCommGroup M₃<VAR>Module R₃ M₃<VAR>ι : Type u_12<VAR>DecidableEq ι<VAR>Fintype ι<VAR>B : LinearMap.BilinForm R₃ M₃<VAR>b : Basis ι R₃ M₃<GOAL>((BilinForm.toMatrix b) B).Nondegenerate ↔ B.Nondegenerate
<VAR>R₃ : Type u_7<VAR>M₃ : Type u_8<VAR>CommRing R₃<VAR>AddCommGroup M₃<VAR>Module R₃ M₃<VAR>ι : Type u_12<VAR>DecidableEq ι<VAR>Fintype ι<VAR>B : LinearMap.BilinForm R₃ M₃<VAR>h : B.Nondegenerate<VAR>b : Basis ι R₃ M₃<GOAL>((BilinForm.toMatrix b) B).Nondegenerate
<VAR>A : Type u_11<VAR>CommRing A<VAR>IsDomain A<VAR>ι : Type u_12<VAR>DecidableEq ι<VAR>Fintype ι<VAR>M : Matrix ι ι A<GOAL>(Matrix.toBilin' M).Nondegenerate ↔ M.det ≠ 0
<VAR>A : Type u_11<VAR>CommRing A<VAR>IsDomain A<VAR>ι : Type u_12<VAR>DecidableEq ι<VAR>Fintype ι<VAR>M : Matrix ι ι A<VAR>h : M.det ≠ 0<GOAL>(Matrix.toBilin' M).Nondegenerate
<VAR>M₃ : Type u_8<VAR>AddCommGroup M₃<VAR>A : Type u_11<VAR>CommRing A<VAR>IsDomain A<VAR>Module A M₃<VAR>ι : Type u_12<VAR>DecidableEq ι<VAR>Fintype ι<VAR>B : LinearMap.BilinForm A M₃<VAR>b : Basis ι A M₃<GOAL>B.Nondegenerate ↔ ((BilinForm.toMatrix b) B).det ≠ 0
<VAR>M₃ : Type u_8<VAR>AddCommGroup M₃<VAR>A : Type u_11<VAR>CommRing A<VAR>IsDomain A<VAR>Module A M₃<VAR>B₃ : LinearMap.BilinForm A M₃<VAR>ι : Type u_12<VAR>DecidableEq ι<VAR>Fintype ι<VAR>b : Basis ι A M₃<VAR>h : ((BilinForm.toMatrix b) B₃).det ≠ 0<GOAL>B₃.Nondegenerate
<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>AffineSpace V P<VAR>ι : Type u_4<VAR>p : ι → P<GOAL>AffineIndependent k p ↔ ∀ (s : Finset ι) (w : ι → k), ∑ i ∈ s, w i = 0 → (s.weightedVSub p) w = 0 → ∀ i ∈ s, w i = 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>AffineSpace V P<VAR>ι : Type u_4<VAR>Subsingleton ι<VAR>p : ι → P<GOAL>AffineIndependent k 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>AffineSpace V P<VAR>ι : Type u_4<VAR>Fintype ι<VAR>p : ι → P<GOAL>AffineIndependent k p ↔ ∀ (w : ι → k), ∑ i : ι, w i = 0 → (Finset.univ.weightedVSub p) w = 0 → ∀ (i : ι), w i = 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>AffineSpace V P<VAR>ι : Type u_4<VAR>p : ι → P<VAR>v : V<GOAL>AffineIndependent k (v +ᵥ p) ↔ AffineIndependent k 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>AffineSpace V P<VAR>ι : Type u_4<VAR>p : ι → P<VAR>i1 : ι<GOAL>AffineIndependent k p ↔ LinearIndependent k fun i => p ↑i -ᵥ p i1
<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>AffineSpace V P<VAR>s : Set P<VAR>p₁ : P<VAR>hp₁ : p₁ ∈ s<GOAL>(AffineIndependent k fun p => ↑p) ↔ LinearIndependent k fun (v : ↑((fun p => p -ᵥ p₁) '' (s \ {p₁}))) => ↑v
<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>AffineSpace V P<VAR>s : Set V<VAR>hs : ∀ v ∈ s, v ≠ 0<VAR>p₁ : P<GOAL>(LinearIndependent k fun (v : ↑s) => ↑v) ↔ AffineIndependent k fun p => ↑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>AffineSpace V P<VAR>ι : Type u_4<VAR>p : ι → P<GOAL>AffineIndependent k p ↔ ∀ (s1 s2 : Finset ι) (w1 w2 : ι → k), ∑ i ∈ s1, w1 i = 1 → ∑ i ∈ s2, w2 i = 1 → (Finset.affineCombination k s1 p) w1 = (Finset.affineCombination k s2 p) w2 → (↑s1).indicator w1 = (↑s2).indicator w2
<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>AffineSpace V P<VAR>ι : Type u_4<VAR>Fintype ι<VAR>p : ι → P<GOAL>AffineIndependent k p ↔ ∀ (w1 w2 : ι → k), ∑ i : ι, w1 i = 1 → ∑ i : ι, w2 i = 1 → (Finset.affineCombination k Finset.univ p) w1 = (Finset.affineCombination k Finset.univ p) w2 → w1 = w2
<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>AffineSpace V P<VAR>ι : Type u_4<VAR>p : ι → P<VAR>hp : AffineIndependent k p<VAR>j : ι<VAR>w : ι → kˣ<GOAL>AffineIndependent k fun i => (AffineMap.lineMap (p j) (p i)) ↑(w 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>AffineSpace V P<VAR>ι : Type u_4<VAR>p : ι → P<VAR>ha : AffineIndependent k p<VAR>s₁ s₂ : Finset ι<VAR>w₁ w₂ : ι → k<VAR>hw₁ : ∑ i ∈ s₁, w₁ i = 1<VAR>hw₂ : ∑ i ∈ s₂, w₂ i = 1<VAR>h : (Finset.affineCombination k s₁ p) w₁ = (Finset.affineCombination k s₂ p) w₂<GOAL>(↑s₁).indicator w₁ = (↑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>AffineSpace V P<VAR>ι : Type u_4<VAR>Nontrivial k<VAR>p : ι → P<VAR>ha : AffineIndependent k p<GOAL>Function.Injective 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>AffineSpace V P<VAR>ι : Type u_4<VAR>ι2 : Type u_5<VAR>f : ι2 ↪ ι<VAR>p : ι → P<VAR>ha : AffineIndependent k p<GOAL>AffineIndependent k (p ∘ ⇑f)
<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>AffineSpace V P<VAR>ι : Type u_4<VAR>p : ι → P<VAR>ha : AffineIndependent k p<VAR>s : Set ι<GOAL>AffineIndependent k fun 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>AffineSpace V P<VAR>ι : Type u_4<VAR>p : ι → P<VAR>ha : AffineIndependent k p<GOAL>AffineIndependent k fun x => ↑x
<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>AffineSpace V P<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>e : ι ≃ ι'<VAR>p : ι' → P<GOAL>AffineIndependent k (p ∘ ⇑e) ↔ AffineIndependent k 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>AffineSpace V P<VAR>s t : Set P<VAR>ha : AffineIndependent k fun x => ↑x<VAR>hs : s ⊆ t<GOAL>AffineIndependent k fun x => ↑x
<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>AffineSpace V P<VAR>ι : Type u_4<VAR>p : ι → P<VAR>ha : AffineIndependent k fun x => ↑x<VAR>hi : Function.Injective p<GOAL>AffineIndependent k 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>AffineSpace V P<VAR>ι : Type u_4<VAR>V₂ : Type u_5<VAR>P₂ : Type u_6<VAR>AddCommGroup V₂<VAR>Module k V₂<VAR>AffineSpace V₂ P₂<VAR>p : ι → P<VAR>f : P →ᵃ[k] P₂<VAR>hai : AffineIndependent k (⇑f ∘ p)<GOAL>AffineIndependent k 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>AffineSpace V P<VAR>ι : Type u_4<VAR>V₂ : Type u_5<VAR>P₂ : Type u_6<VAR>AddCommGroup V₂<VAR>Module k V₂<VAR>AffineSpace V₂ P₂<VAR>p : ι → P<VAR>hai : AffineIndependent k p<VAR>f : P →ᵃ[k] P₂<VAR>hf : Function.Injective ⇑f<GOAL>AffineIndependent k (⇑f ∘ 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>AffineSpace V P<VAR>ι : Type u_4<VAR>V₂ : Type u_5<VAR>P₂ : Type u_6<VAR>AddCommGroup V₂<VAR>Module k V₂<VAR>AffineSpace V₂ P₂<VAR>p : ι → P<VAR>f : P →ᵃ[k] P₂<VAR>hf : Function.Injective ⇑f<GOAL>AffineIndependent k (⇑f ∘ p) ↔ AffineIndependent k 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>AffineSpace V P<VAR>ι : Type u_4<VAR>V₂ : Type u_5<VAR>P₂ : Type u_6<VAR>AddCommGroup V₂<VAR>Module k V₂<VAR>AffineSpace V₂ P₂<VAR>p : ι → P<VAR>e : P ≃ᵃ[k] P₂<GOAL>AffineIndependent k (⇑e ∘ p) ↔ AffineIndependent k 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>AffineSpace V P<VAR>V₂ : Type u_5<VAR>P₂ : Type u_6<VAR>AddCommGroup V₂<VAR>Module k V₂<VAR>AffineSpace V₂ P₂<VAR>s : Set P<VAR>e : P ≃ᵃ[k] P₂<GOAL>AffineIndependent k Subtype.val ↔ AffineIndependent k Subtype.val
<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>AffineSpace V P<VAR>ι : Type u_4<VAR>Nontrivial k<VAR>p : ι → P<VAR>ha : AffineIndependent k p<VAR>s1 s2 : Set ι<VAR>p0 : P<VAR>hp0s1 : p0 ∈ affineSpan k (p '' s1)<VAR>hp0s2 : p0 ∈ affineSpan k (p '' s2)<GOAL>∃ i, i ∈ s1 ∩ s2
<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>AffineSpace V P<VAR>ι : Type u_4<VAR>Nontrivial k<VAR>p : ι → P<VAR>ha : AffineIndependent k p<VAR>s1 s2 : Set ι<VAR>hd : Disjoint s1 s2<GOAL>Disjoint ↑(affineSpan k (p '' s1)) ↑(affineSpan k (p '' s2))
<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>AffineSpace V P<VAR>ι : Type u_4<VAR>Nontrivial k<VAR>p : ι → P<VAR>ha : AffineIndependent k p<VAR>i : ι<VAR>s : Set ι<GOAL>p i ∈ affineSpan k (p '' s) ↔ i ∈ s
<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>AffineSpace V P<VAR>ι : Type u_4<VAR>Nontrivial k<VAR>p : ι → P<VAR>ha : AffineIndependent k p<VAR>i : ι<VAR>s : Set ι<GOAL>p i ∉ affineSpan k (p '' (s \ {i}))
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>t : Finset V<VAR>h : ¬AffineIndependent k Subtype.val<GOAL>∃ f, ∑ e ∈ t, f e • e = 0 ∧ ∑ e ∈ t, f e = 0 ∧ ∃ x ∈ t, f x ≠ 0
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>ι : Type u_5<VAR>p : ι → V<GOAL>AffineIndependent k p ↔ ∀ (s : Finset ι) (w : ι → k), s.sum w = 0 → ∑ e ∈ s, w e • p e = 0 → ∀ e ∈ s, w e = 0
<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>w : ι → k<VAR>p : ι → V<VAR>hp : AffineIndependent k p<VAR>hw₀ : ∑ i ∈ s, w i = 0<VAR>hw₁ : ∑ i ∈ s, w i • p i = 0<VAR>i : ι<GOAL>i ∈ s → w i = 0
<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>w₁ w₂ : ι → k<VAR>p : ι → V<VAR>hp : AffineIndependent k p<VAR>hw : ∑ i ∈ s, w₁ i = ∑ i ∈ s, w₂ i<VAR>hwp : ∑ i ∈ s, w₁ i • p i = ∑ i ∈ s, w₂ i • p i<VAR>i : ι<GOAL>i ∈ s → w₁ i = w₂ i
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>s : Finset V<VAR>hp : AffineIndependent k Subtype.val<VAR>w : V → k<VAR>hw₀ : ∑ x ∈ s, w x = 0<VAR>hw₁ : ∑ x ∈ s, w x • x = 0<VAR>x : V<GOAL>x ∈ s → w x = 0
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>s : Finset V<VAR>hp : AffineIndependent k Subtype.val<VAR>w₁ w₂ : V → k<VAR>hw : ∑ i ∈ s, w₁ i = ∑ i ∈ s, w₂ i<VAR>hwp : ∑ i ∈ s, w₁ i • i = ∑ i ∈ s, w₂ i • i<VAR>i : V<GOAL>i ∈ s → w₁ i = w₂ 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>AffineSpace V P<VAR>ι : Type u_4<VAR>p : ι → P<VAR>h : AffineIndependent k p<VAR>w w₁ w₂ : ι → k<VAR>s : Finset ι<VAR>hw : ∑ i ∈ s, w i = 0<VAR>hw₁ : ∑ i ∈ s, w₁ i = 1<VAR>hw₂ : ∑ i ∈ s, w₂ i = 1<GOAL>(s.weightedVSub p) w ∈ vectorSpan k {(Finset.affineCombination k s p) w₁, (Finset.affineCombination k s p) w₂} ↔ ∃ r, ∀ i ∈ s, w i = r * (w₁ i - w₂ 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>AffineSpace V P<VAR>ι : Type u_4<VAR>p : ι → P<VAR>h : AffineIndependent k p<VAR>w w₁ w₂ : ι → k<VAR>s : Finset ι<GOAL>∑ i ∈ s, w i = 1 → ∑ i ∈ s, w₁ i = 1 → ∑ i ∈ s, w₂ i = 1 → ((Finset.affineCombination k s p) w ∈ affineSpan k {(Finset.affineCombination k s p) w₁, (Finset.affineCombination k s p) w₂} ↔ ∃ r, ∀ i ∈ s, w i = r * (w₂ i - w₁ i) + w₁ 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>s : Set P<VAR>h : AffineIndependent k fun p => ↑p<GOAL>∃ t, s ⊆ t ∧ (AffineIndependent k fun p => ↑p) ∧ affineSpan k t = ⊤
<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>∃ t ⊆ s, affineSpan k t = affineSpan k s ∧ AffineIndependent k Subtype.val
<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<VAR>h : p₁ ≠ p₂<GOAL>AffineIndependent 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>ι : Type u_4<VAR>p : ι → P<VAR>i : ι<VAR>ha : AffineIndependent k fun x => p ↑x<VAR>hi : p i ∉ affineSpan k (p '' {x | x ≠ i})<GOAL>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>s : AffineSubspace k P<VAR>p₁ p₂ p₃ : P<VAR>hp₁p₂ : p₁ ≠ p₂<VAR>hp₁ : p₁ ∈ s<VAR>hp₂ : p₂ ∈ s<VAR>hp₃ : p₃ ∉ s<GOAL>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>s : AffineSubspace k P<VAR>p₁ p₂ p₃ : P<VAR>hp₁p₃ : p₁ ≠ p₃<VAR>hp₁ : p₁ ∈ s<VAR>hp₂ : p₂ ∉ s<VAR>hp₃ : p₃ ∈ s<GOAL>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>s : AffineSubspace k P<VAR>p₁ p₂ p₃ : P<VAR>hp₂p₃ : p₂ ≠ p₃<VAR>hp₁ : p₁ ∉ s<VAR>hp₂ : p₂ ∈ s<VAR>hp₃ : p₃ ∈ s<GOAL>AffineIndependent k ![p₁, p₂, p₃]
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>LinearOrderedRing k<VAR>AddCommGroup V<VAR>Module k V<VAR>AffineSpace V P<VAR>ι : Type u_4<VAR>p : ι → P<VAR>h : AffineIndependent k p<VAR>w w₁ w₂ : ι → k<VAR>s : Finset ι<VAR>hw : ∑ i ∈ s, w i = 1<VAR>hw₁ : ∑ i ∈ s, w₁ i = 1<VAR>hw₂ : ∑ i ∈ s, w₂ i = 1<VAR>hs : (Finset.affineCombination k s p) w ∈ affineSpan k {(Finset.affineCombination k s p) w₁, (Finset.affineCombination k s p) w₂}<VAR>i j : ι<VAR>hi : i ∈ s<VAR>hj : j ∈ s<VAR>hi0 : w₁ i = 0<VAR>hj0 : w₁ j = 0<VAR>hij : SignType.sign (w₂ i) = SignType.sign (w₂ j)<GOAL>SignType.sign (w i) = SignType.sign (w j)
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>LinearOrderedRing k<VAR>AddCommGroup V<VAR>Module k V<VAR>AffineSpace V P<VAR>ι : Type u_4<VAR>p : ι → P<VAR>h : AffineIndependent k p<VAR>w : ι → k<VAR>s : Finset ι<VAR>hw : ∑ i ∈ s, w i = 1<VAR>i₁ i₂ i₃ : ι<VAR>h₁ : i₁ ∈ s<VAR>h₂ : i₂ ∈ s<VAR>h₃ : i₃ ∈ s<VAR>h₁₂ : i₁ ≠ i₂<VAR>h₁₃ : i₁ ≠ i₃<VAR>h₂₃ : i₂ ≠ i₃<VAR>c : k<VAR>hc0 : 0 < c<VAR>hc1 : c < 1<VAR>hs : (Finset.affineCombination k s p) w ∈ affineSpan k {p i₁, (AffineMap.lineMap (p i₂) (p i₃)) c}<GOAL>SignType.sign (w i₂) = SignType.sign (w 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>AffineSpace V P<VAR>n : ℕ<VAR>self : Affine.Simplex k P n<GOAL>AffineIndependent k self.points
<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>AffineSpace V P<VAR>p : P<VAR>i : Fin 1<GOAL>(Affine.Simplex.mkOfPoint k p).points i = 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>AffineSpace V P<VAR>n : ℕ<VAR>s1 s2 : Affine.Simplex k P n<VAR>h : ∀ (i : Fin (n + 1)), s1.points i = s2.points i<GOAL>s1 = s2
<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>AffineSpace V P<VAR>n : ℕ<VAR>s1 s2 : Affine.Simplex k P n<GOAL>s1 = s2 ↔ ∀ (i : Fin (n + 1)), s1.points i = s2.points 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>AffineSpace V P<VAR>n : ℕ<VAR>s : Affine.Simplex k P n<VAR>fs : Finset (Fin (n + 1))<VAR>m : ℕ<VAR>h : fs.card = m + 1<VAR>i : Fin (m + 1)<GOAL>(s.face h).points i = s.points ((fs.orderEmbOfFin h) i)