ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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.affineCombination k (Finset.map e s₂) p) w = (Finset.affineCombination k s₂ (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) = (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>p₂ : P<VAR>h : ∑ i ∈ s, w i = 1<GOAL>∑ i ∈ s, w i • (p₁ i -ᵥ p₂) = (Finset.affineCombination k s 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 : ι → k<VAR>p₂ : ι → P<VAR>p₁ : P<VAR>h : ∑ i ∈ s, w i = 1<GOAL>∑ i ∈ s, w i • (p₁ -ᵥ p₂ i) = p₁ -ᵥ (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>DecidableEq ι<VAR>s₂ : Finset ι<VAR>h : s₂ ⊆ s<VAR>w : ι → k<VAR>p : ι → P<GOAL>(Finset.affineCombination k (s \ s₂) p) w -ᵥ (Finset.affineCombination k s₂ 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>hw : (s.weightedVSub p) w = 0<VAR>i : ι<VAR>DecidablePred fun x => x ≠ i<VAR>his : i ∈ s<VAR>hwi : w i = -1<GOAL>(Finset.affineCombination k (Finset.filter (fun x => x ≠ i) 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>s : Finset ι<VAR>w : ι → k<VAR>p : ι → P<VAR>pred : ι → Prop<VAR>DecidablePred pred<GOAL>((Finset.affineCombination k (Finset.subtype pred s) fun i => p ↑i) fun i => w ↑i) = (Finset.affineCombination k (Finset.filter pred 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>pred : ι → Prop<VAR>DecidablePred pred<VAR>h : ∀ i ∈ s, w i ≠ 0 → pred i<GOAL>(Finset.affineCombination k (Finset.filter pred 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>v : V<VAR>x : k<VAR>s : Set ι<VAR>p : ι → P<VAR>b : P<GOAL>(∃ fs, ↑fs ⊆ s ∧ ∃ w, ∑ i ∈ fs, w i = x ∧ v = (fs.weightedVSubOfPoint p b) w) ↔ ∃ fs w, ∑ i ∈ fs, w i = x ∧ v = (fs.weightedVSubOfPoint (fun i => p ↑i) 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>v : V<VAR>s : Set ι<VAR>p : ι → P<GOAL>(∃ fs, ↑fs ⊆ s ∧ ∃ w, ∑ i ∈ fs, w i = 0 ∧ v = (fs.weightedVSub p) w) ↔ ∃ fs w, ∑ i ∈ fs, w i = 0 ∧ v = (fs.weightedVSub fun i => 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>p0 : P<VAR>s : Set ι<VAR>p : ι → P<GOAL>(∃ fs, ↑fs ⊆ s ∧ ∃ w, ∑ i ∈ fs, w i = 1 ∧ p0 = (Finset.affineCombination k fs p) w) ↔ ∃ fs w, ∑ i ∈ fs, w i = 1 ∧ p0 = (Finset.affineCombination k fs fun i => 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>V₂ : Type u_6<VAR>P₂ : Type u_7<VAR>AddCommGroup V₂<VAR>Module k V₂<VAR>AffineSpace V₂ P₂<VAR>p : ι → P<VAR>w : ι → k<VAR>hw : s.sum w = 1<VAR>f : P →ᵃ[k] P₂<GOAL>f ((Finset.affineCombination k s p) w) = (Finset.affineCombination k s (⇑f ∘ p)) w
<VAR>k : Type u_1<VAR>Ring k<VAR>ι : Type u_4<VAR>DecidableEq ι<VAR>i : ι<GOAL>Finset.affineCombinationSingleWeights k i i = 1
<VAR>k : Type u_1<VAR>Ring k<VAR>ι : Type u_4<VAR>DecidableEq ι<VAR>i j : ι<VAR>h : j ≠ i<GOAL>Finset.affineCombinationSingleWeights k i j = 0
<VAR>k : Type u_1<VAR>Ring k<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>DecidableEq ι<VAR>i : ι<VAR>h : i ∈ s<GOAL>∑ j ∈ s, Finset.affineCombinationSingleWeights k i j = 1
<VAR>k : Type u_1<VAR>Ring k<VAR>ι : Type u_4<VAR>DecidableEq ι<VAR>i : ι<GOAL>Finset.weightedVSubVSubWeights k i i = 0
<VAR>k : Type u_1<VAR>Ring k<VAR>ι : Type u_4<VAR>DecidableEq ι<VAR>i j : ι<VAR>h : i ≠ j<GOAL>Finset.weightedVSubVSubWeights k i j i = 1
<VAR>k : Type u_1<VAR>Ring k<VAR>ι : Type u_4<VAR>DecidableEq ι<VAR>i j : ι<VAR>h : i ≠ j<GOAL>Finset.weightedVSubVSubWeights k i j j = -1
<VAR>k : Type u_1<VAR>Ring k<VAR>ι : Type u_4<VAR>DecidableEq ι<VAR>i j t : ι<VAR>hi : t ≠ i<VAR>hj : t ≠ j<GOAL>Finset.weightedVSubVSubWeights k i j t = 0
<VAR>k : Type u_1<VAR>Ring k<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>DecidableEq ι<VAR>i j : ι<VAR>hi : i ∈ s<VAR>hj : j ∈ s<GOAL>∑ t ∈ s, Finset.weightedVSubVSubWeights k i j t = 0
<VAR>k : Type u_1<VAR>Ring k<VAR>ι : Type u_4<VAR>DecidableEq ι<VAR>i : ι<VAR>c : k<GOAL>Finset.affineCombinationLineMapWeights i i c = Finset.affineCombinationSingleWeights k i
<VAR>k : Type u_1<VAR>Ring k<VAR>ι : Type u_4<VAR>DecidableEq ι<VAR>i j : ι<VAR>h : i ≠ j<VAR>c : k<GOAL>Finset.affineCombinationLineMapWeights i j c i = 1 - c
<VAR>k : Type u_1<VAR>Ring k<VAR>ι : Type u_4<VAR>DecidableEq ι<VAR>i j : ι<VAR>h : i ≠ j<VAR>c : k<GOAL>Finset.affineCombinationLineMapWeights i j c j = c
<VAR>k : Type u_1<VAR>Ring k<VAR>ι : Type u_4<VAR>DecidableEq ι<VAR>i j t : ι<VAR>hi : t ≠ i<VAR>hj : t ≠ j<VAR>c : k<GOAL>Finset.affineCombinationLineMapWeights i j c t = 0
<VAR>k : Type u_1<VAR>Ring k<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>DecidableEq ι<VAR>i j : ι<VAR>hi : i ∈ s<VAR>hj : j ∈ s<VAR>c : k<GOAL>∑ t ∈ s, Finset.affineCombinationLineMapWeights i j c t = 1
<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>p : ι → P<VAR>i : ι<VAR>hi : i ∈ s<GOAL>(Finset.affineCombination k s p) (Finset.affineCombinationSingleWeights k 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>DecidableEq ι<VAR>p : ι → P<VAR>i j : ι<VAR>hi : i ∈ s<VAR>hj : j ∈ s<GOAL>(s.weightedVSub p) (Finset.weightedVSubVSubWeights k i j) = p i -ᵥ p j
<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>p : ι → P<VAR>i j : ι<VAR>hi : i ∈ s<VAR>hj : j ∈ s<VAR>c : k<GOAL>(Finset.affineCombination k s p) (Finset.affineCombinationLineMapWeights i j c) = (AffineMap.lineMap (p i) (p j)) c
<VAR>k : Type u_1<VAR>DivisionRing k<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>i : ι<GOAL>Finset.centroidWeights k s i = (↑s.card)⁻¹
<VAR>k : Type u_1<VAR>DivisionRing k<VAR>ι : Type u_4<VAR>s : Finset ι<GOAL>Finset.centroidWeights k s = Function.const ι (↑s.card)⁻¹
<VAR>k : Type u_1<VAR>DivisionRing k<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>h : ↑s.card ≠ 0<GOAL>∑ i ∈ s, Finset.centroidWeights k s i = 1
<VAR>k : Type u_1<VAR>DivisionRing k<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>CharZero k<VAR>h : s.card ≠ 0<GOAL>∑ i ∈ s, Finset.centroidWeights k s i = 1
<VAR>k : Type u_1<VAR>DivisionRing k<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>CharZero k<VAR>h : s.Nonempty<GOAL>∑ i ∈ s, Finset.centroidWeights k s i = 1
<VAR>k : Type u_1<VAR>DivisionRing k<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>CharZero k<VAR>n : ℕ<VAR>h : s.card = n + 1<GOAL>∑ i ∈ s, Finset.centroidWeights k s i = 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>ι : Type u_4<VAR>s : Finset ι<VAR>p : ι → P<GOAL>Finset.centroid k s p = (Finset.affineCombination k s p) (Finset.centroidWeights 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 : Finset P<GOAL>Finset.centroid k Finset.univ Subtype.val = Finset.centroid k s id
<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 : ι<GOAL>Finset.centroid k {i} p = 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>ι : Type u_4<VAR>DecidableEq ι<VAR>Invertible 2<VAR>p : ι → P<VAR>i₁ i₂ : ι<GOAL>Finset.centroid k {i₁, i₂} p = 2⁻¹ • (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>Invertible 2<VAR>p : Fin 2 → P<GOAL>Finset.centroid k Finset.univ p = 2⁻¹ • (p 1 -ᵥ p 0) +ᵥ p 0
<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>ι₂ : Type u_5<VAR>s₂ : Finset ι₂<VAR>e : ι₂ ↪ ι<VAR>p : ι → P<GOAL>Finset.centroid k (Finset.map e s₂) p = Finset.centroid k s₂ (p ∘ ⇑e)
<VAR>k : Type u_1<VAR>DivisionRing k<VAR>ι : Type u_4<VAR>s : Finset ι<GOAL>Finset.centroidWeightsIndicator k s = (↑s).indicator (Finset.centroidWeights k s)
<VAR>k : Type u_1<VAR>DivisionRing k<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>Fintype ι<GOAL>∑ i : ι, Finset.centroidWeightsIndicator k s i = ∑ i ∈ s, Finset.centroidWeights k s i
<VAR>k : Type u_1<VAR>DivisionRing k<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>CharZero k<VAR>Fintype ι<VAR>h : s.card ≠ 0<GOAL>∑ i : ι, Finset.centroidWeightsIndicator k s i = 1
<VAR>k : Type u_1<VAR>DivisionRing k<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>CharZero k<VAR>Fintype ι<VAR>h : s.Nonempty<GOAL>∑ i : ι, Finset.centroidWeightsIndicator k s i = 1
<VAR>k : Type u_1<VAR>DivisionRing k<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>CharZero k<VAR>Fintype ι<VAR>n : ℕ<VAR>h : s.card = n + 1<GOAL>∑ i : ι, Finset.centroidWeightsIndicator k s i = 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>ι : Type u_4<VAR>s : Finset ι<VAR>Fintype ι<VAR>p : ι → P<GOAL>Finset.centroid k s p = (Finset.affineCombination k Finset.univ p) (Finset.centroidWeightsIndicator 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>ι : Type u_4<VAR>s : Finset ι<VAR>p : ι → P<VAR>hi : ∀ i ∈ s, ∀ j ∈ s, p i = p j → i = j<VAR>ps : Set P<VAR>Fintype ↑ps<VAR>hps : ps = p '' ↑s<GOAL>Finset.centroid k s p = Finset.centroid k Finset.univ fun x => ↑x
<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>s : Finset ι<VAR>ι₂ : Type u_5<VAR>s₂ : Finset ι₂<VAR>p : ι → P<VAR>hi : ∀ i ∈ s, ∀ j ∈ s, p i = p j → i = j<VAR>p₂ : ι₂ → P<VAR>hi₂ : ∀ i ∈ s₂, ∀ j ∈ s₂, p₂ i = p₂ j → i = j<VAR>he : p '' ↑s = p₂ '' ↑s₂<GOAL>Finset.centroid k s p = Finset.centroid k s₂ p₂
<VAR>ι : Type u_1<VAR>k : Type u_2<VAR>V : Type u_3<VAR>P : Type u_4<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>AffineSpace V P<VAR>s : Finset ι<VAR>w : ι → k<VAR>h : ∑ i ∈ s, w i = 0<VAR>p : ι → P<GOAL>(s.weightedVSub p) w ∈ vectorSpan k (Set.range p)
<VAR>ι : Type u_1<VAR>k : Type u_2<VAR>V : Type u_3<VAR>P : Type u_4<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>AffineSpace V P<VAR>Nontrivial k<VAR>s : Finset ι<VAR>w : ι → k<VAR>h : ∑ i ∈ s, w i = 1<VAR>p : ι → P<GOAL>(Finset.affineCombination k s p) w ∈ affineSpan k (Set.range p)
<VAR>ι : Type u_1<VAR>k : Type u_2<VAR>V : Type u_3<VAR>P : Type u_4<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>AffineSpace V P<VAR>v : V<VAR>p : ι → P<GOAL>v ∈ vectorSpan k (Set.range p) ↔ ∃ s w, ∑ i ∈ s, w i = 0 ∧ v = (s.weightedVSub p) w
<VAR>ι : Type u_1<VAR>k : Type u_2<VAR>V : Type u_3<VAR>P : Type u_4<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>AffineSpace V P<VAR>p1 : P<VAR>p : ι → P<VAR>h : p1 ∈ affineSpan k (Set.range p)<GOAL>∃ s w, ∑ i ∈ s, w i = 1 ∧ p1 = (Finset.affineCombination k s p) w
<VAR>ι : Type u_1<VAR>k : Type u_2<VAR>V : Type u_3<VAR>P : Type u_4<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>AffineSpace V P<VAR>Fintype ι<VAR>p1 : P<VAR>p : ι → P<VAR>h : p1 ∈ affineSpan k (Set.range p)<GOAL>∃ w, ∑ i : ι, w i = 1 ∧ p1 = (Finset.affineCombination k Finset.univ p) w
<VAR>ι : Type u_1<VAR>k : Type u_2<VAR>V : Type u_3<VAR>P : Type u_4<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>AffineSpace V P<VAR>Nontrivial k<VAR>p1 : P<VAR>p : ι → P<GOAL>p1 ∈ affineSpan k (Set.range p) ↔ ∃ s w, ∑ i ∈ s, w i = 1 ∧ p1 = (Finset.affineCombination k s p) w
<VAR>ι : Type u_1<VAR>k : Type u_2<VAR>V : Type u_3<VAR>P : Type u_4<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>AffineSpace V P<VAR>Nontrivial k<VAR>p : ι → P<VAR>j : ι<VAR>q : P<GOAL>q ∈ affineSpan k (Set.range p) ↔ ∃ s w, q = (s.weightedVSubOfPoint p (p j)) w +ᵥ p j
<VAR>k : Type u_2<VAR>V : Type u_3<VAR>P : Type u_4<VAR>Ring k<VAR>AddCommGroup V<VAR>Module k V<VAR>AffineSpace V P<VAR>Nontrivial k<VAR>s : Set P<VAR>p : P<VAR>hp : p ∈ s<VAR>w : ↑s → kˣ<GOAL>affineSpan k (Set.range fun q => (AffineMap.lineMap p ↑q) ↑(w q)) = 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>ι : Type u_4<VAR>s : Finset ι<VAR>p : ι → P<VAR>h : ↑s.card ≠ 0<GOAL>Finset.centroid k s p ∈ affineSpan 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>ι : Type u_4<VAR>CharZero k<VAR>s : Finset ι<VAR>p : ι → P<VAR>h : s.card ≠ 0<GOAL>Finset.centroid k s p ∈ affineSpan 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>ι : Type u_4<VAR>CharZero k<VAR>s : Finset ι<VAR>p : ι → P<VAR>h : s.Nonempty<GOAL>Finset.centroid k s p ∈ affineSpan 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>ι : Type u_4<VAR>CharZero k<VAR>s : Finset ι<VAR>p : ι → P<VAR>n : ℕ<VAR>h : s.card = n + 1<GOAL>Finset.centroid k s p ∈ affineSpan k (Set.range p)
<VAR>k : Type u_1<VAR>V1 : Type u_2<VAR>P1 : Type u_3<VAR>V2 : Type u_4<VAR>P2 : Type u_5<VAR>Ring k<VAR>AddCommGroup V1<VAR>Module k V1<VAR>AffineSpace V1 P1<VAR>AddCommGroup V2<VAR>Module k V2<VAR>AffineSpace V2 P2<VAR>self : P1 →ᵃ[k] P2<VAR>p : P1<VAR>v : V1<GOAL>self.toFun (v +ᵥ p) = self.linear v +ᵥ self.toFun p
<VAR>k : Type u_1<VAR>V₁ : Type u_2<VAR>V₂ : Type u_3<VAR>Ring k<VAR>AddCommGroup V₁<VAR>Module k V₁<VAR>AddCommGroup V₂<VAR>Module k V₂<VAR>f : V₁ →ₗ[k] V₂<GOAL>⇑f.toAffineMap = ⇑f
<VAR>k : Type u_1<VAR>V₁ : Type u_2<VAR>V₂ : Type u_3<VAR>Ring k<VAR>AddCommGroup V₁<VAR>Module k V₁<VAR>AddCommGroup V₂<VAR>Module k V₂<VAR>f : V₁ →ₗ[k] V₂<GOAL>f.toAffineMap.linear = f
<VAR>k : Type u_1<VAR>V1 : Type u_2<VAR>P1 : Type u_3<VAR>V2 : Type u_4<VAR>P2 : Type u_5<VAR>Ring k<VAR>AddCommGroup V1<VAR>Module k V1<VAR>AffineSpace V1 P1<VAR>AddCommGroup V2<VAR>Module k V2<VAR>AffineSpace V2 P2<VAR>f : P1 → P2<VAR>linear : V1 →ₗ[k] V2<VAR>add : ∀ (p : P1) (v : V1), f (v +ᵥ p) = linear v +ᵥ f p<GOAL>⇑{ toFun := f, linear := linear, map_vadd' := add } = f
<VAR>k : Type u_1<VAR>V1 : Type u_2<VAR>P1 : Type u_3<VAR>V2 : Type u_4<VAR>P2 : Type u_5<VAR>Ring k<VAR>AddCommGroup V1<VAR>Module k V1<VAR>AffineSpace V1 P1<VAR>AddCommGroup V2<VAR>Module k V2<VAR>AffineSpace V2 P2<VAR>f : P1 →ᵃ[k] P2<GOAL>f.toFun = ⇑f
<VAR>k : Type u_1<VAR>V1 : Type u_2<VAR>P1 : Type u_3<VAR>V2 : Type u_4<VAR>P2 : Type u_5<VAR>Ring k<VAR>AddCommGroup V1<VAR>Module k V1<VAR>AffineSpace V1 P1<VAR>AddCommGroup V2<VAR>Module k V2<VAR>AffineSpace V2 P2<VAR>f : P1 →ᵃ[k] P2<VAR>p : P1<VAR>v : V1<GOAL>f (v +ᵥ p) = f.linear v +ᵥ f p
<VAR>k : Type u_1<VAR>V1 : Type u_2<VAR>P1 : Type u_3<VAR>V2 : Type u_4<VAR>P2 : Type u_5<VAR>Ring k<VAR>AddCommGroup V1<VAR>Module k V1<VAR>AffineSpace V1 P1<VAR>AddCommGroup V2<VAR>Module k V2<VAR>AffineSpace V2 P2<VAR>f : P1 →ᵃ[k] P2<VAR>p1 p2 : P1<GOAL>f.linear (p1 -ᵥ p2) = f p1 -ᵥ f p2
<VAR>k : Type u_1<VAR>V1 : Type u_2<VAR>P1 : Type u_3<VAR>V2 : Type u_4<VAR>P2 : Type u_5<VAR>Ring k<VAR>AddCommGroup V1<VAR>Module k V1<VAR>AffineSpace V1 P1<VAR>AddCommGroup V2<VAR>Module k V2<VAR>AffineSpace V2 P2<VAR>f g : P1 →ᵃ[k] P2<VAR>h : ∀ (p : P1), f p = g p<GOAL>f = g
<VAR>k : Type u_1<VAR>V1 : Type u_2<VAR>P1 : Type u_3<VAR>V2 : Type u_4<VAR>P2 : Type u_5<VAR>Ring k<VAR>AddCommGroup V1<VAR>Module k V1<VAR>AffineSpace V1 P1<VAR>AddCommGroup V2<VAR>Module k V2<VAR>AffineSpace V2 P2<VAR>f g : P1 →ᵃ[k] P2<GOAL>f = g ↔ ∀ (p : P1), f p = g p
<VAR>k : Type u_1<VAR>V1 : Type u_2<VAR>P1 : Type u_3<VAR>V2 : Type u_4<VAR>P2 : Type u_5<VAR>Ring k<VAR>AddCommGroup V1<VAR>Module k V1<VAR>AffineSpace V1 P1<VAR>AddCommGroup V2<VAR>Module k V2<VAR>AffineSpace V2 P2<GOAL>Function.Injective DFunLike.coe
<VAR>k : Type u_1<VAR>V1 : Type u_2<VAR>P1 : Type u_3<VAR>V2 : Type u_4<VAR>P2 : Type u_5<VAR>Ring k<VAR>AddCommGroup V1<VAR>Module k V1<VAR>AffineSpace V1 P1<VAR>AddCommGroup V2<VAR>Module k V2<VAR>AffineSpace V2 P2<VAR>f : P1 →ᵃ[k] P2<VAR>x y : P1<VAR>h : x = y<GOAL>f x = f y
<VAR>k : Type u_1<VAR>V1 : Type u_2<VAR>P1 : Type u_3<VAR>V2 : Type u_4<VAR>P2 : Type u_5<VAR>Ring k<VAR>AddCommGroup V1<VAR>Module k V1<VAR>AffineSpace V1 P1<VAR>AddCommGroup V2<VAR>Module k V2<VAR>AffineSpace V2 P2<VAR>f g : P1 →ᵃ[k] P2<VAR>h : f = g<VAR>x : P1<GOAL>f x = g x
<VAR>k : Type u_1<VAR>V1 : Type u_2<VAR>P1 : Type u_3<VAR>V2 : Type u_4<VAR>P2 : Type u_5<VAR>Ring k<VAR>AddCommGroup V1<VAR>Module k V1<VAR>AffineSpace V1 P1<VAR>AddCommGroup V2<VAR>Module k V2<VAR>AffineSpace V2 P2<VAR>f g : P1 →ᵃ[k] P2<VAR>h₁ : f.linear = g.linear<VAR>p : P1<VAR>h₂ : f p = g p<GOAL>f = g
<VAR>k : Type u_1<VAR>V1 : Type u_2<VAR>P1 : Type u_3<VAR>V2 : Type u_4<VAR>P2 : Type u_5<VAR>Ring k<VAR>AddCommGroup V1<VAR>Module k V1<VAR>AffineSpace V1 P1<VAR>AddCommGroup V2<VAR>Module k V2<VAR>AffineSpace V2 P2<VAR>f g : P1 →ᵃ[k] P2<GOAL>f = g ↔ f.linear = g.linear ∧ ∃ p, f p = g p
<VAR>k : Type u_1<VAR>V1 : Type u_2<VAR>P1 : Type u_3<VAR>V2 : Type u_4<VAR>P2 : Type u_5<VAR>Ring k<VAR>AddCommGroup V1<VAR>Module k V1<VAR>AffineSpace V1 P1<VAR>AddCommGroup V2<VAR>Module k V2<VAR>AffineSpace V2 P2<VAR>p : P2<GOAL>⇑(AffineMap.const k P1 p) = Function.const P1 p
<VAR>k : Type u_1<VAR>V1 : Type u_2<VAR>P1 : Type u_3<VAR>V2 : Type u_4<VAR>P2 : Type u_5<VAR>Ring k<VAR>AddCommGroup V1<VAR>Module k V1<VAR>AffineSpace V1 P1<VAR>AddCommGroup V2<VAR>Module k V2<VAR>AffineSpace V2 P2<VAR>p : P2<VAR>q : P1<GOAL>(AffineMap.const k P1 p) q = p
<VAR>k : Type u_1<VAR>V1 : Type u_2<VAR>P1 : Type u_3<VAR>V2 : Type u_4<VAR>P2 : Type u_5<VAR>Ring k<VAR>AddCommGroup V1<VAR>Module k V1<VAR>AffineSpace V1 P1<VAR>AddCommGroup V2<VAR>Module k V2<VAR>AffineSpace V2 P2<VAR>p : P2<GOAL>(AffineMap.const k P1 p).linear = 0
<VAR>k : Type u_1<VAR>V1 : Type u_2<VAR>P1 : Type u_3<VAR>V2 : Type u_4<VAR>P2 : Type u_5<VAR>Ring k<VAR>AddCommGroup V1<VAR>Module k V1<VAR>AffineSpace V1 P1<VAR>AddCommGroup V2<VAR>Module k V2<VAR>AffineSpace V2 P2<VAR>f : P1 →ᵃ[k] P2<GOAL>f.linear = 0 ↔ ∃ q, f = AffineMap.const k P1 q
<VAR>k : Type u_1<VAR>V1 : Type u_2<VAR>P1 : Type u_3<VAR>V2 : Type u_4<VAR>P2 : Type u_5<VAR>Ring k<VAR>AddCommGroup V1<VAR>Module k V1<VAR>AffineSpace V1 P1<VAR>AddCommGroup V2<VAR>Module k V2<VAR>AffineSpace V2 P2<VAR>f : P1 → P2<VAR>f' : V1 →ₗ[k] V2<VAR>p : P1<VAR>h : ∀ (p' : P1), f p' = f' (p' -ᵥ p) +ᵥ f p<GOAL>⇑(AffineMap.mk' f f' p h) = f
<VAR>k : Type u_1<VAR>V1 : Type u_2<VAR>P1 : Type u_3<VAR>V2 : Type u_4<VAR>P2 : Type u_5<VAR>Ring k<VAR>AddCommGroup V1<VAR>Module k V1<VAR>AffineSpace V1 P1<VAR>AddCommGroup V2<VAR>Module k V2<VAR>AffineSpace V2 P2<VAR>f : P1 → P2<VAR>f' : V1 →ₗ[k] V2<VAR>p : P1<VAR>h : ∀ (p' : P1), f p' = f' (p' -ᵥ p) +ᵥ f p<GOAL>(AffineMap.mk' f f' p h).linear = f'
<VAR>k : Type u_1<VAR>V1 : Type u_2<VAR>P1 : Type u_3<VAR>V2 : Type u_4<VAR>Ring k<VAR>AddCommGroup V1<VAR>Module k V1<VAR>AffineSpace V1 P1<VAR>AddCommGroup V2<VAR>Module k V2<VAR>R : Type u_10<VAR>Monoid R<VAR>DistribMulAction R V2<VAR>SMulCommClass k R V2<VAR>c : R<VAR>f : P1 →ᵃ[k] V2<GOAL>⇑(c • f) = c • ⇑f
<VAR>k : Type u_1<VAR>V1 : Type u_2<VAR>P1 : Type u_3<VAR>V2 : Type u_4<VAR>Ring k<VAR>AddCommGroup V1<VAR>Module k V1<VAR>AffineSpace V1 P1<VAR>AddCommGroup V2<VAR>Module k V2<VAR>R : Type u_10<VAR>Monoid R<VAR>DistribMulAction R V2<VAR>SMulCommClass k R V2<VAR>t : R<VAR>f : P1 →ᵃ[k] V2<GOAL>(t • f).linear = t • f.linear
<VAR>k : Type u_1<VAR>V1 : Type u_2<VAR>P1 : Type u_3<VAR>V2 : Type u_4<VAR>Ring k<VAR>AddCommGroup V1<VAR>Module k V1<VAR>AffineSpace V1 P1<VAR>AddCommGroup V2<VAR>Module k V2<GOAL>⇑0 = 0
<VAR>k : Type u_1<VAR>V1 : Type u_2<VAR>P1 : Type u_3<VAR>V2 : Type u_4<VAR>Ring k<VAR>AddCommGroup V1<VAR>Module k V1<VAR>AffineSpace V1 P1<VAR>AddCommGroup V2<VAR>Module k V2<VAR>f g : P1 →ᵃ[k] V2<GOAL>⇑(f + g) = ⇑f + ⇑g
<VAR>k : Type u_1<VAR>V1 : Type u_2<VAR>P1 : Type u_3<VAR>V2 : Type u_4<VAR>Ring k<VAR>AddCommGroup V1<VAR>Module k V1<VAR>AffineSpace V1 P1<VAR>AddCommGroup V2<VAR>Module k V2<VAR>f : P1 →ᵃ[k] V2<GOAL>⇑(-f) = -⇑f
<VAR>k : Type u_1<VAR>V1 : Type u_2<VAR>P1 : Type u_3<VAR>V2 : Type u_4<VAR>Ring k<VAR>AddCommGroup V1<VAR>Module k V1<VAR>AffineSpace V1 P1<VAR>AddCommGroup V2<VAR>Module k V2<VAR>f g : P1 →ᵃ[k] V2<GOAL>⇑(f - g) = ⇑f - ⇑g
<VAR>k : Type u_1<VAR>V1 : Type u_2<VAR>P1 : Type u_3<VAR>V2 : Type u_4<VAR>Ring k<VAR>AddCommGroup V1<VAR>Module k V1<VAR>AffineSpace V1 P1<VAR>AddCommGroup V2<VAR>Module k V2<GOAL>AffineMap.linear 0 = 0
<VAR>k : Type u_1<VAR>V1 : Type u_2<VAR>P1 : Type u_3<VAR>V2 : Type u_4<VAR>Ring k<VAR>AddCommGroup V1<VAR>Module k V1<VAR>AffineSpace V1 P1<VAR>AddCommGroup V2<VAR>Module k V2<VAR>f g : P1 →ᵃ[k] V2<GOAL>(f + g).linear = f.linear + g.linear
<VAR>k : Type u_1<VAR>V1 : Type u_2<VAR>P1 : Type u_3<VAR>V2 : Type u_4<VAR>Ring k<VAR>AddCommGroup V1<VAR>Module k V1<VAR>AffineSpace V1 P1<VAR>AddCommGroup V2<VAR>Module k V2<VAR>f g : P1 →ᵃ[k] V2<GOAL>(f - g).linear = f.linear - g.linear
<VAR>k : Type u_1<VAR>V1 : Type u_2<VAR>P1 : Type u_3<VAR>V2 : Type u_4<VAR>Ring k<VAR>AddCommGroup V1<VAR>Module k V1<VAR>AffineSpace V1 P1<VAR>AddCommGroup V2<VAR>Module k V2<VAR>f : P1 →ᵃ[k] V2<GOAL>(-f).linear = -f.linear
<VAR>k : Type u_1<VAR>V1 : Type u_2<VAR>P1 : Type u_3<VAR>V2 : Type u_4<VAR>P2 : Type u_5<VAR>Ring k<VAR>AddCommGroup V1<VAR>Module k V1<VAR>AffineSpace V1 P1<VAR>AddCommGroup V2<VAR>Module k V2<VAR>AffineSpace V2 P2<VAR>f : P1 →ᵃ[k] V2<VAR>g : P1 →ᵃ[k] P2<VAR>p : P1<GOAL>(f +ᵥ g) p = f p +ᵥ g p
<VAR>k : Type u_1<VAR>V1 : Type u_2<VAR>P1 : Type u_3<VAR>V2 : Type u_4<VAR>P2 : Type u_5<VAR>Ring k<VAR>AddCommGroup V1<VAR>Module k V1<VAR>AffineSpace V1 P1<VAR>AddCommGroup V2<VAR>Module k V2<VAR>AffineSpace V2 P2<VAR>f g : P1 →ᵃ[k] P2<VAR>p : P1<GOAL>(f -ᵥ g) p = f p -ᵥ g p
<VAR>k : Type u_1<VAR>V1 : Type u_2<VAR>P1 : Type u_3<VAR>V2 : Type u_4<VAR>P2 : Type u_5<VAR>Ring k<VAR>AddCommGroup V1<VAR>Module k V1<VAR>AffineSpace V1 P1<VAR>AddCommGroup V2<VAR>Module k V2<VAR>AffineSpace V2 P2<GOAL>⇑AffineMap.fst = Prod.fst
<VAR>k : Type u_1<VAR>V1 : Type u_2<VAR>P1 : Type u_3<VAR>V2 : Type u_4<VAR>P2 : Type u_5<VAR>Ring k<VAR>AddCommGroup V1<VAR>Module k V1<VAR>AffineSpace V1 P1<VAR>AddCommGroup V2<VAR>Module k V2<VAR>AffineSpace V2 P2<GOAL>AffineMap.fst.linear = LinearMap.fst k V1 V2
<VAR>k : Type u_1<VAR>V1 : Type u_2<VAR>P1 : Type u_3<VAR>V2 : Type u_4<VAR>P2 : Type u_5<VAR>Ring k<VAR>AddCommGroup V1<VAR>Module k V1<VAR>AffineSpace V1 P1<VAR>AddCommGroup V2<VAR>Module k V2<VAR>AffineSpace V2 P2<GOAL>⇑AffineMap.snd = Prod.snd
<VAR>k : Type u_1<VAR>V1 : Type u_2<VAR>P1 : Type u_3<VAR>V2 : Type u_4<VAR>P2 : Type u_5<VAR>Ring k<VAR>AddCommGroup V1<VAR>Module k V1<VAR>AffineSpace V1 P1<VAR>AddCommGroup V2<VAR>Module k V2<VAR>AffineSpace V2 P2<GOAL>AffineMap.snd.linear = LinearMap.snd k V1 V2
<VAR>k : Type u_1<VAR>V1 : Type u_2<VAR>P1 : Type u_3<VAR>Ring k<VAR>AddCommGroup V1<VAR>Module k V1<VAR>AffineSpace V1 P1<GOAL>⇑(AffineMap.id k P1) = id