ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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).linear = LinearMap.id
<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<VAR>p : P1<GOAL>(AffineMap.id k P1) p = 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>V3 : Type u_6<VAR>P3 : Type u_7<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>AddCommGroup V3<VAR>Module k V3<VAR>AffineSpace V3 P3<VAR>f : P2 →ᵃ[k] P3<VAR>g : P1 →ᵃ[k] P2<GOAL>⇑(f.comp g) = ⇑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>V3 : Type u_6<VAR>P3 : Type u_7<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>AddCommGroup V3<VAR>Module k V3<VAR>AffineSpace V3 P3<VAR>f : P2 →ᵃ[k] P3<VAR>g : P1 →ᵃ[k] P2<VAR>p : P1<GOAL>(f.comp g) p = f (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 : P1 →ᵃ[k] P2<GOAL>f.comp (AffineMap.id k P1) = 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>(AffineMap.id k P2).comp f = 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>V3 : Type u_6<VAR>P3 : Type u_7<VAR>V4 : Type u_8<VAR>P4 : Type u_9<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>AddCommGroup V3<VAR>Module k V3<VAR>AffineSpace V3 P3<VAR>AddCommGroup V4<VAR>Module k V4<VAR>AffineSpace V4 P4<VAR>f₃₄ : P3 →ᵃ[k] P4<VAR>f₂₃ : P2 →ᵃ[k] P3<VAR>f₁₂ : P1 →ᵃ[k] P2<GOAL>(f₃₄.comp f₂₃).comp f₁₂ = f₃₄.comp (f₂₃.comp f₁₂)
<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<VAR>f g : P1 →ᵃ[k] P1<GOAL>⇑(f * g) = ⇑f ∘ ⇑g
<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>⇑1 = id
<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<VAR>self : P1 →ᵃ[k] P1<GOAL>AffineMap.linearHom self = self.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] P2<GOAL>Function.Injective ⇑f.linear ↔ Function.Injective ⇑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>Function.Surjective ⇑f.linear ↔ Function.Surjective ⇑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>Function.Bijective ⇑f.linear ↔ Function.Bijective ⇑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>s t : Set P1<VAR>f : P1 →ᵃ[k] P2<GOAL>⇑f '' s -ᵥ ⇑f '' t = ⇑f.linear '' (s -ᵥ t)
<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<VAR>p₀ p₁ : P1<GOAL>⇑(AffineMap.lineMap p₀ p₁) = fun c => c • (p₁ -ᵥ p₀) +ᵥ p₀
<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<VAR>p₀ p₁ : P1<VAR>c : k<GOAL>(AffineMap.lineMap p₀ p₁) c = c • (p₁ -ᵥ p₀) +ᵥ p₀
<VAR>k : Type u_1<VAR>V1 : Type u_2<VAR>Ring k<VAR>AddCommGroup V1<VAR>Module k V1<VAR>p₀ p₁ : V1<VAR>c : k<GOAL>(AffineMap.lineMap p₀ p₁) c = c • (p₁ - p₀) + p₀
<VAR>k : Type u_1<VAR>V1 : Type u_2<VAR>Ring k<VAR>AddCommGroup V1<VAR>Module k V1<VAR>p₀ p₁ : V1<VAR>c : k<GOAL>(AffineMap.lineMap p₀ p₁) c = (1 - c) • p₀ + c • p₁
<VAR>k : Type u_1<VAR>Ring k<VAR>a b c : k<GOAL>(AffineMap.lineMap a b) c = c * (b - a) + a
<VAR>k : Type u_1<VAR>Ring k<VAR>a b c : k<GOAL>(AffineMap.lineMap a b) c = (1 - c) * a + c * b
<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<VAR>p : P1<VAR>v : V1<VAR>c : k<GOAL>(AffineMap.lineMap p (v +ᵥ p)) c = c • v +ᵥ p
<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<VAR>p₀ p₁ : P1<GOAL>(AffineMap.lineMap p₀ p₁).linear = LinearMap.id.smulRight (p₁ -ᵥ p₀)
<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<VAR>p : P1<VAR>c : k<GOAL>(AffineMap.lineMap p p) c = p
<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<VAR>p : P1<GOAL>AffineMap.lineMap p p = AffineMap.const k k p
<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<VAR>p₀ p₁ : P1<GOAL>(AffineMap.lineMap p₀ p₁) 0 = p₀
<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<VAR>p₀ p₁ : P1<GOAL>(AffineMap.lineMap p₀ p₁) 1 = p₁
<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<VAR>NoZeroSMulDivisors k V1<VAR>p₀ p₁ : P1<VAR>c₁ c₂ : k<GOAL>(AffineMap.lineMap p₀ p₁) c₁ = (AffineMap.lineMap p₀ p₁) c₂ ↔ p₀ = p₁ ∨ c₁ = c₂
<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<VAR>NoZeroSMulDivisors k V1<VAR>p₀ p₁ : P1<VAR>c : k<GOAL>(AffineMap.lineMap p₀ p₁) c = p₀ ↔ p₀ = p₁ ∨ c = 0
<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<VAR>NoZeroSMulDivisors k V1<VAR>p₀ p₁ : P1<VAR>c : k<GOAL>(AffineMap.lineMap p₀ p₁) c = p₁ ↔ p₀ = p₁ ∨ c = 1
<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<VAR>NoZeroSMulDivisors k V1<VAR>p₀ p₁ : P1<VAR>h : p₀ ≠ p₁<GOAL>Function.Injective ⇑(AffineMap.lineMap p₀ 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>p₀ p₁ : P1<VAR>c : k<GOAL>f ((AffineMap.lineMap p₀ p₁) c) = (AffineMap.lineMap (f p₀) (f p₁)) c
<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₀ p₁ : P1<GOAL>f.comp (AffineMap.lineMap p₀ p₁) = AffineMap.lineMap (f p₀) (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>p₀ p₁ : P1 × P2<VAR>c : k<GOAL>((AffineMap.lineMap p₀ p₁) c).1 = (AffineMap.lineMap p₀.1 p₁.1) c
<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₀ p₁ : P1 × P2<VAR>c : k<GOAL>((AffineMap.lineMap p₀ p₁) c).2 = (AffineMap.lineMap p₀.2 p₁.2) c
<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<VAR>p₀ p₁ : P1<GOAL>AffineMap.lineMap p₀ p₁ = (AffineMap.lineMap p₁ p₀).comp (AffineMap.lineMap 1 0)
<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<VAR>p₀ p₁ : P1<VAR>c : k<GOAL>(AffineMap.lineMap p₀ p₁) (1 - c) = (AffineMap.lineMap p₁ p₀) c
<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<VAR>p₀ p₁ : P1<VAR>c : k<GOAL>(AffineMap.lineMap p₀ p₁) c -ᵥ p₀ = c • (p₁ -ᵥ p₀)
<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<VAR>p₀ p₁ : P1<VAR>c : k<GOAL>p₀ -ᵥ (AffineMap.lineMap p₀ p₁) c = c • (p₀ -ᵥ p₁)
<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<VAR>p₀ p₁ : P1<VAR>c : k<GOAL>(AffineMap.lineMap p₀ p₁) c -ᵥ p₁ = (1 - c) • (p₀ -ᵥ p₁)
<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<VAR>p₀ p₁ : P1<VAR>c : k<GOAL>p₁ -ᵥ (AffineMap.lineMap p₀ p₁) c = (1 - c) • (p₁ -ᵥ p₀)
<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<VAR>v₁ v₂ : V1<VAR>p₁ p₂ : P1<VAR>c : k<GOAL>(AffineMap.lineMap v₁ v₂) c +ᵥ (AffineMap.lineMap p₁ p₂) c = (AffineMap.lineMap (v₁ +ᵥ p₁) (v₂ +ᵥ p₂)) c
<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<VAR>p₁ p₂ p₃ p₄ : P1<VAR>c : k<GOAL>(AffineMap.lineMap p₁ p₂) c -ᵥ (AffineMap.lineMap p₃ p₄) c = (AffineMap.lineMap (p₁ -ᵥ p₃) (p₂ -ᵥ p₄)) c
<VAR>k : Type u_1<VAR>V1 : Type u_2<VAR>V2 : Type u_4<VAR>Ring k<VAR>AddCommGroup V1<VAR>Module k V1<VAR>AddCommGroup V2<VAR>Module k V2<VAR>f : V1 →ᵃ[k] V2<GOAL>⇑f = ⇑f.linear + fun x => f 0
<VAR>k : Type u_1<VAR>V1 : Type u_2<VAR>V2 : Type u_4<VAR>Ring k<VAR>AddCommGroup V1<VAR>Module k V1<VAR>AddCommGroup V2<VAR>Module k V2<VAR>f : V1 →ᵃ[k] V2<GOAL>⇑f.linear = ⇑f - fun x => f 0
<VAR>k : Type u_10<VAR>LinearOrderedField k<VAR>f : k →ᵃ[k] k<VAR>a b : k<GOAL>⇑f '' Set.uIcc a b = Set.uIcc (f a) (f b)
<VAR>k : Type u_1<VAR>Ring k<VAR>ι : Type u_10<VAR>V : ι → Type u_11<VAR>P : ι → Type u_12<VAR>(i : ι) → AddCommGroup (V i)<VAR>(i : ι) → Module k (V i)<VAR>(i : ι) → AffineSpace (V i) (P i)<VAR>i : ι<VAR>f : (i : ι) → P i<GOAL>(AffineMap.proj i) f = f i
<VAR>k : Type u_1<VAR>Ring k<VAR>ι : Type u_10<VAR>V : ι → Type u_11<VAR>P : ι → Type u_12<VAR>(i : ι) → AddCommGroup (V i)<VAR>(i : ι) → Module k (V i)<VAR>(i : ι) → AffineSpace (V i) (P i)<VAR>i : ι<GOAL>(AffineMap.proj i).linear = LinearMap.proj i
<VAR>k : Type u_1<VAR>Ring k<VAR>ι : Type u_10<VAR>V : ι → Type u_11<VAR>P : ι → Type u_12<VAR>(i : ι) → AddCommGroup (V i)<VAR>(i : ι) → Module k (V i)<VAR>(i : ι) → AffineSpace (V i) (P i)<VAR>f g : (i : ι) → P i<VAR>c : k<VAR>i : ι<GOAL>(AffineMap.lineMap f g) c i = (AffineMap.lineMap (f i) (g i)) c
<VAR>R : Type u_1<VAR>k : Type u_2<VAR>V1 : Type u_3<VAR>V2 : Type u_5<VAR>Ring k<VAR>AddCommGroup V1<VAR>AddCommGroup V2<VAR>Module k V1<VAR>Module k V2<VAR>Semiring R<VAR>Module R V2<VAR>SMulCommClass k R V2<VAR>f : V1 →ᵃ[k] V2<GOAL>(AffineMap.toConstProdLinearMap R) f = (f 0, f.linear)
<VAR>R : Type u_1<VAR>k : Type u_2<VAR>V1 : Type u_3<VAR>V2 : Type u_5<VAR>Ring k<VAR>AddCommGroup V1<VAR>AddCommGroup V2<VAR>Module k V1<VAR>Module k V2<VAR>Semiring R<VAR>Module R V2<VAR>SMulCommClass k R V2<VAR>p : V2 × (V1 →ₗ[k] V2)<GOAL>(AffineMap.toConstProdLinearMap R).symm p = p.2.toAffineMap + AffineMap.const k V1 p.1
<VAR>k : Type u_2<VAR>V1 : Type u_3<VAR>P1 : Type u_4<VAR>Ring k<VAR>AddCommGroup V1<VAR>AffineSpace V1 P1<VAR>Module k V1<VAR>ι : Type u_9<VAR>φv : ι → Type u_10<VAR>φp : ι → Type u_11<VAR>(i : ι) → AddCommGroup (φv i)<VAR>(i : ι) → Module k (φv i)<VAR>(i : ι) → AffineSpace (φv i) (φp i)<VAR>fp : (i : ι) → P1 →ᵃ[k] φp i<VAR>c : P1<VAR>i : ι<GOAL>(AffineMap.pi fp) c i = (fp i) c
<VAR>k : Type u_2<VAR>V1 : Type u_3<VAR>P1 : Type u_4<VAR>V3 : Type u_7<VAR>P3 : Type u_8<VAR>Ring k<VAR>AddCommGroup V1<VAR>AffineSpace V1 P1<VAR>AddCommGroup V3<VAR>AffineSpace V3 P3<VAR>Module k V1<VAR>Module k V3<VAR>ι : Type u_9<VAR>φv : ι → Type u_10<VAR>φp : ι → Type u_11<VAR>(i : ι) → AddCommGroup (φv i)<VAR>(i : ι) → Module k (φv i)<VAR>(i : ι) → AffineSpace (φv i) (φp i)<VAR>fp : (i : ι) → P1 →ᵃ[k] φp i<VAR>g : P3 →ᵃ[k] P1<GOAL>(AffineMap.pi fp).comp g = AffineMap.pi fun i => (fp i).comp g
<VAR>k : Type u_2<VAR>V1 : Type u_3<VAR>P1 : Type u_4<VAR>Ring k<VAR>AddCommGroup V1<VAR>AffineSpace V1 P1<VAR>Module k V1<VAR>ι : Type u_9<VAR>φv : ι → Type u_10<VAR>(i : ι) → AddCommGroup (φv i)<VAR>(i : ι) → Module k (φv i)<VAR>fv : (i : ι) → P1 →ᵃ[k] φv i<GOAL>AffineMap.pi fv = 0 ↔ ∀ (i : ι), fv i = 0
<VAR>k : Type u_2<VAR>V1 : Type u_3<VAR>P1 : Type u_4<VAR>Ring k<VAR>AddCommGroup V1<VAR>AffineSpace V1 P1<VAR>Module k V1<VAR>ι : Type u_9<VAR>φv : ι → Type u_10<VAR>(i : ι) → AddCommGroup (φv i)<VAR>(i : ι) → Module k (φv i)<GOAL>(AffineMap.pi fun x => 0) = 0
<VAR>k : Type u_2<VAR>V1 : Type u_3<VAR>P1 : Type u_4<VAR>Ring k<VAR>AddCommGroup V1<VAR>AffineSpace V1 P1<VAR>Module k V1<VAR>ι : Type u_9<VAR>φv : ι → Type u_10<VAR>φp : ι → Type u_11<VAR>(i : ι) → AddCommGroup (φv i)<VAR>(i : ι) → Module k (φv i)<VAR>(i : ι) → AffineSpace (φv i) (φp i)<VAR>fp : (i : ι) → P1 →ᵃ[k] φp i<VAR>i : ι<GOAL>(AffineMap.proj i).comp (AffineMap.pi fp) = fp i
<VAR>k : Type u_2<VAR>V2 : Type u_5<VAR>P2 : Type u_6<VAR>Ring k<VAR>AddCommGroup V2<VAR>AffineSpace V2 P2<VAR>Module k V2<VAR>ι : Type u_9<VAR>φv : ι → Type u_10<VAR>(i : ι) → AddCommGroup (φv i)<VAR>(i : ι) → Module k (φv i)<VAR>Finite ι<VAR>DecidableEq ι<VAR>f g : ((i : ι) → φv i) →ᵃ[k] P2<VAR>h : ∀ (i : ι) (x : φv i), f (Pi.single i x) = g (Pi.single i x)<VAR>h₂ : f 0 = g 0<GOAL>f = g
<VAR>k : Type u_2<VAR>V2 : Type u_5<VAR>P2 : Type u_6<VAR>Ring k<VAR>AddCommGroup V2<VAR>AffineSpace V2 P2<VAR>Module k V2<VAR>ι : Type u_9<VAR>φv : ι → Type u_10<VAR>(i : ι) → AddCommGroup (φv i)<VAR>(i : ι) → Module k (φv i)<VAR>Finite ι<VAR>DecidableEq ι<VAR>f g : ((i : ι) → φv i) →ᵃ[k] P2<VAR>Nonempty ι<VAR>h : ∀ (i : ι) (x : φv i), f (Pi.single i x) = g (Pi.single i x)<GOAL>f = g
<VAR>k : Type u_2<VAR>V2 : Type u_5<VAR>P2 : Type u_6<VAR>Ring k<VAR>AddCommGroup V2<VAR>AffineSpace V2 P2<VAR>Module k V2<VAR>ι : Type u_9<VAR>φv : ι → Type u_10<VAR>(i : ι) → AddCommGroup (φv i)<VAR>(i : ι) → Module k (φv i)<VAR>Finite ι<VAR>DecidableEq ι<VAR>f g : ((i : ι) → φv i) →ᵃ[k] P2<VAR>Nonempty ι<VAR>h : ∀ (i : ι), f.comp (LinearMap.single i).toAffineMap = g.comp (LinearMap.single i).toAffineMap<GOAL>f = g
<VAR>k : Type u_2<VAR>V1 : Type u_3<VAR>P1 : Type u_4<VAR>CommRing k<VAR>AddCommGroup V1<VAR>AffineSpace V1 P1<VAR>Module k V1<VAR>c : P1<VAR>r : k<GOAL>AffineMap.homothety c r = r • (AffineMap.id k P1 -ᵥ AffineMap.const k P1 c) +ᵥ AffineMap.const k P1 c
<VAR>k : Type u_2<VAR>V1 : Type u_3<VAR>P1 : Type u_4<VAR>CommRing k<VAR>AddCommGroup V1<VAR>AffineSpace V1 P1<VAR>Module k V1<VAR>c : P1<VAR>r : k<VAR>p : P1<GOAL>(AffineMap.homothety c r) p = r • (p -ᵥ c) +ᵥ c
<VAR>k : Type u_2<VAR>V1 : Type u_3<VAR>P1 : Type u_4<VAR>CommRing k<VAR>AddCommGroup V1<VAR>AffineSpace V1 P1<VAR>Module k V1<VAR>c : P1<VAR>r : k<VAR>p : P1<GOAL>(AffineMap.homothety c r) p = (AffineMap.lineMap c p) r
<VAR>k : Type u_2<VAR>V1 : Type u_3<VAR>P1 : Type u_4<VAR>CommRing k<VAR>AddCommGroup V1<VAR>AffineSpace V1 P1<VAR>Module k V1<VAR>c : P1<GOAL>AffineMap.homothety c 1 = AffineMap.id k P1
<VAR>k : Type u_2<VAR>V1 : Type u_3<VAR>P1 : Type u_4<VAR>CommRing k<VAR>AddCommGroup V1<VAR>AffineSpace V1 P1<VAR>Module k V1<VAR>c : P1<VAR>r : k<GOAL>(AffineMap.homothety c r) c = c
<VAR>k : Type u_2<VAR>V1 : Type u_3<VAR>P1 : Type u_4<VAR>CommRing k<VAR>AddCommGroup V1<VAR>AffineSpace V1 P1<VAR>Module k V1<VAR>c : P1<VAR>r₁ r₂ : k<VAR>p : P1<GOAL>(AffineMap.homothety c (r₁ * r₂)) p = (AffineMap.homothety c r₁) ((AffineMap.homothety c r₂) p)
<VAR>k : Type u_2<VAR>V1 : Type u_3<VAR>P1 : Type u_4<VAR>CommRing k<VAR>AddCommGroup V1<VAR>AffineSpace V1 P1<VAR>Module k V1<VAR>c : P1<VAR>r₁ r₂ : k<GOAL>AffineMap.homothety c (r₁ * r₂) = (AffineMap.homothety c r₁).comp (AffineMap.homothety c r₂)
<VAR>k : Type u_2<VAR>V1 : Type u_3<VAR>P1 : Type u_4<VAR>CommRing k<VAR>AddCommGroup V1<VAR>AffineSpace V1 P1<VAR>Module k V1<VAR>c : P1<GOAL>AffineMap.homothety c 0 = AffineMap.const k P1 c
<VAR>k : Type u_2<VAR>V1 : Type u_3<VAR>P1 : Type u_4<VAR>CommRing k<VAR>AddCommGroup V1<VAR>AffineSpace V1 P1<VAR>Module k V1<VAR>c : P1<VAR>r₁ r₂ : k<GOAL>AffineMap.homothety c (r₁ + r₂) = r₁ • (AffineMap.id k P1 -ᵥ AffineMap.const k P1 c) +ᵥ AffineMap.homothety c r₂
<VAR>k : Type u_2<VAR>V1 : Type u_3<VAR>P1 : Type u_4<VAR>CommRing k<VAR>AddCommGroup V1<VAR>AffineSpace V1 P1<VAR>Module k V1<VAR>c : P1<GOAL>⇑(AffineMap.homothetyHom c) = AffineMap.homothety c
<VAR>k : Type u_2<VAR>V1 : Type u_3<VAR>P1 : Type u_4<VAR>CommRing k<VAR>AddCommGroup V1<VAR>AffineSpace V1 P1<VAR>Module k V1<VAR>c : P1<GOAL>⇑(AffineMap.homothetyAffine c) = AffineMap.homothety c
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>Ring 𝕜<VAR>AddCommGroup E<VAR>AddCommGroup F<VAR>Module 𝕜 E<VAR>Module 𝕜 F<VAR>x y : E<VAR>a b : 𝕜<VAR>f : E →ᵃ[𝕜] F<VAR>h : a + b = 1<GOAL>f (a • x + b • y) = a • f x + b • f y
<VAR>R : Type u_1<VAR>Field R<VAR>a b : R<VAR>hab : a ^ 2 + b ^ 2 ≠ 0<GOAL>↑(Matrix.planeConformalMatrix a b hab) = !![a, -b; b, a]
<VAR>α : Type u_1<VAR>n : Type u_2<VAR>m : Type u_3<VAR>Mul α<VAR>AddCommMonoid α<VAR>A : Matrix m n α<VAR>Fintype m<GOAL>A.transpose.HasOrthogonalRows ↔ A.HasOrthogonalCols
<VAR>α : Type u_1<VAR>n : Type u_2<VAR>m : Type u_3<VAR>Mul α<VAR>AddCommMonoid α<VAR>A : Matrix m n α<VAR>Fintype n<GOAL>A.transpose.HasOrthogonalCols ↔ A.HasOrthogonalRows
<VAR>α : Type u_1<VAR>n : Type u_2<VAR>m : Type u_3<VAR>Mul α<VAR>AddCommMonoid α<VAR>A : Matrix m n α<VAR>Fintype m<VAR>h : A.transpose.HasOrthogonalRows<GOAL>A.HasOrthogonalCols
<VAR>α : Type u_1<VAR>n : Type u_2<VAR>m : Type u_3<VAR>Mul α<VAR>AddCommMonoid α<VAR>A : Matrix m n α<VAR>Fintype m<VAR>h : A.HasOrthogonalCols<GOAL>A.transpose.HasOrthogonalRows
<VAR>α : Type u_1<VAR>n : Type u_2<VAR>m : Type u_3<VAR>Mul α<VAR>AddCommMonoid α<VAR>A : Matrix m n α<VAR>Fintype n<VAR>h : A.transpose.HasOrthogonalCols<GOAL>A.HasOrthogonalRows
<VAR>α : Type u_1<VAR>n : Type u_2<VAR>m : Type u_3<VAR>Mul α<VAR>AddCommMonoid α<VAR>A : Matrix m n α<VAR>Fintype n<VAR>h : A.HasOrthogonalRows<GOAL>A.transpose.HasOrthogonalCols
<VAR>K : Type u_1<VAR>V₁ : Type u_2<VAR>V₂ : Type u_3<VAR>ι₁ : Type u_4<VAR>ι₂ : Type u_5<VAR>Field K<VAR>AddCommGroup V₁<VAR>Module K V₁<VAR>AddCommGroup V₂<VAR>Module K V₂<VAR>Fintype ι₁<VAR>Fintype ι₂<VAR>DecidableEq ι₁<VAR>DecidableEq ι₂<VAR>B₁ : Basis ι₁ K V₁<VAR>B₂ : Basis ι₂ K V₂<VAR>u : V₁ →ₗ[K] V₂<GOAL>(LinearMap.toMatrix B₂.dualBasis B₁.dualBasis) (Module.Dual.transpose u) = ((LinearMap.toMatrix B₁ B₂) u)ᵀ
<VAR>K : Type u_1<VAR>V₁ : Type u_2<VAR>V₂ : Type u_3<VAR>ι₁ : Type u_4<VAR>ι₂ : Type u_5<VAR>Field K<VAR>AddCommGroup V₁<VAR>Module K V₁<VAR>AddCommGroup V₂<VAR>Module K V₂<VAR>Fintype ι₁<VAR>Fintype ι₂<VAR>DecidableEq ι₁<VAR>DecidableEq ι₂<VAR>B₁ : Basis ι₁ K V₁<VAR>B₂ : Basis ι₂ K V₂<VAR>M : Matrix ι₁ ι₂ K<GOAL>(Matrix.toLin B₁.dualBasis B₂.dualBasis) Mᵀ = Module.Dual.transpose ((Matrix.toLin B₂ B₁) M)
<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<GOAL>vectorSpan k s = Submodule.span k (s -ᵥ 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>s₁ s₂ : Set P<VAR>h : s₁ ⊆ s₂<GOAL>vectorSpan k s₁ ≤ vectorSpan k 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<GOAL>vectorSpan k ∅ = ⊥
<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<GOAL>vectorSpan 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 : Set P<GOAL>s -ᵥ s ⊆ ↑(vectorSpan k 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>s : Set P<VAR>p1 p2 : P<VAR>hp1 : p1 ∈ s<VAR>hp2 : p2 ∈ s<GOAL>p1 -ᵥ p2 ∈ vectorSpan k 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>p : P<VAR>s : Set P<GOAL>p ∈ s → p ∈ spanPoints k 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>s : Set P<GOAL>s ⊆ spanPoints k 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>s : Set P<GOAL>(spanPoints k s).Nonempty ↔ s.Nonempty
<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>v : V<VAR>hp : p ∈ spanPoints k s<VAR>hv : v ∈ vectorSpan k s<GOAL>v +ᵥ p ∈ spanPoints k 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>s : Set P<VAR>p1 p2 : P<VAR>hp1 : p1 ∈ spanPoints k s<VAR>hp2 : p2 ∈ spanPoints k s<GOAL>p1 -ᵥ p2 ∈ vectorSpan k 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>self : AffineSubspace k P<VAR>c : k<VAR>p1 p2 p3 : P<GOAL>p1 ∈ self.carrier → p2 ∈ self.carrier → p3 ∈ self.carrier → c • (p1 -ᵥ p2) +ᵥ p3 ∈ self.carrier
<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>s : AffineSubspace k P<GOAL>p ∈ ↑s ↔ p ∈ 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>s : AffineSubspace k P<GOAL>s.direction = vectorSpan k ↑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>s : AffineSubspace k P<VAR>h : (↑s).Nonempty<GOAL>AffineSubspace.directionOfNonempty h = s.direction
<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 : AffineSubspace k P<VAR>h : (↑s).Nonempty<GOAL>↑s.direction = ↑s -ᵥ ↑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>s : AffineSubspace k P<VAR>h : (↑s).Nonempty<VAR>v : V<GOAL>v ∈ s.direction ↔ ∃ p1 ∈ s, ∃ p2 ∈ s, v = p1 -ᵥ p2
<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 : AffineSubspace k P<VAR>v : V<VAR>hv : v ∈ s.direction<VAR>p : P<VAR>hp : p ∈ s<GOAL>v +ᵥ p ∈ 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>s : AffineSubspace k P<VAR>p1 p2 : P<VAR>hp1 : p1 ∈ s<VAR>hp2 : p2 ∈ s<GOAL>p1 -ᵥ p2 ∈ s.direction
<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 : AffineSubspace k P<VAR>v : V<VAR>p : P<VAR>hp : p ∈ s<GOAL>v +ᵥ p ∈ s ↔ v ∈ s.direction
<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 : AffineSubspace k P<VAR>v : V<VAR>hv : v ∈ s.direction<VAR>p : P<GOAL>v +ᵥ p ∈ s ↔ p ∈ 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>s : AffineSubspace k P<VAR>p : P<VAR>hp : p ∈ s<GOAL>↑s.direction = (fun x => x -ᵥ p) '' ↑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>s : AffineSubspace k P<VAR>p : P<VAR>hp : p ∈ s<GOAL>↑s.direction = (fun x => p -ᵥ x) '' ↑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>s : AffineSubspace k P<VAR>p : P<VAR>hp : p ∈ s<VAR>v : V<GOAL>v ∈ s.direction ↔ ∃ p2 ∈ s, v = p2 -ᵥ p