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>AffineSpace V P<VAR>s1 s2 : AffineSubspace k P<VAR>p1 p2 : P<VAR>hp1 : p1 ∈ s1<VAR>hp2 : p2 ∈ s2<GOAL>(s1 ⊔ s2).direction = s1.direction ⊔ s2.direction ⊔ Submodule.span k {p2 -ᵥ p1}
<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<GOAL>(affineSpan k (insert p2 ↑s)).direction = Submodule.span k {p2 -ᵥ p1} ⊔ 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>p1 : P<VAR>hp1 : p1 ∈ s<VAR>p2 p : P<GOAL>p ∈ affineSpan k (insert p2 ↑s) ↔ ∃ r, ∃ p0 ∈ s, p = r • (p2 -ᵥ p1) +ᵥ p0
<VAR>k : Type u_1<VAR>V₁ : Type u_2<VAR>P₁ : Type u_3<VAR>V₂ : Type u_4<VAR>P₂ : Type u_5<VAR>Ring k<VAR>AddCommGroup V₁<VAR>Module k V₁<VAR>AffineSpace V₁ P₁<VAR>AddCommGroup V₂<VAR>Module k V₂<VAR>AffineSpace V₂ P₂<VAR>f : P₁ →ᵃ[k] P₂<VAR>s : Set P₁<GOAL>Submodule.map f.linear (vectorSpan k s) = vectorSpan k (⇑f '' s)
<VAR>k : Type u_1<VAR>V₁ : Type u_2<VAR>P₁ : Type u_3<VAR>V₂ : Type u_4<VAR>P₂ : Type u_5<VAR>Ring k<VAR>AddCommGroup V₁<VAR>Module k V₁<VAR>AffineSpace V₁ P₁<VAR>AddCommGroup V₂<VAR>Module k V₂<VAR>AffineSpace V₂ P₂<VAR>f : P₁ →ᵃ[k] P₂<VAR>s : AffineSubspace k P₁<GOAL>↑(AffineSubspace.map f s) = ⇑f '' ↑s
<VAR>k : Type u_1<VAR>V₁ : Type u_2<VAR>P₁ : Type u_3<VAR>V₂ : Type u_4<VAR>P₂ : Type u_5<VAR>Ring k<VAR>AddCommGroup V₁<VAR>Module k V₁<VAR>AffineSpace V₁ P₁<VAR>AddCommGroup V₂<VAR>Module k V₂<VAR>AffineSpace V₂ P₂<VAR>f : P₁ →ᵃ[k] P₂<VAR>x : P₂<VAR>s : AffineSubspace k P₁<GOAL>x ∈ AffineSubspace.map f s ↔ ∃ y ∈ s, f y = x
<VAR>k : Type u_1<VAR>V₁ : Type u_2<VAR>P₁ : Type u_3<VAR>V₂ : Type u_4<VAR>P₂ : Type u_5<VAR>Ring k<VAR>AddCommGroup V₁<VAR>Module k V₁<VAR>AffineSpace V₁ P₁<VAR>AddCommGroup V₂<VAR>Module k V₂<VAR>AffineSpace V₂ P₂<VAR>f : P₁ →ᵃ[k] P₂<VAR>x : P₁<VAR>s : AffineSubspace k P₁<VAR>h : x ∈ s<GOAL>f x ∈ AffineSubspace.map f s
<VAR>k : Type u_1<VAR>V₁ : Type u_2<VAR>P₁ : Type u_3<VAR>V₂ : Type u_4<VAR>P₂ : Type u_5<VAR>Ring k<VAR>AddCommGroup V₁<VAR>Module k V₁<VAR>AffineSpace V₁ P₁<VAR>AddCommGroup V₂<VAR>Module k V₂<VAR>AffineSpace V₂ P₂<VAR>f : P₁ →ᵃ[k] P₂<VAR>x : P₁<VAR>s : AffineSubspace k P₁<VAR>hf : Function.Injective ⇑f<GOAL>f x ∈ AffineSubspace.map f s ↔ x ∈ s
<VAR>k : Type u_1<VAR>V₁ : Type u_2<VAR>P₁ : Type u_3<VAR>V₂ : Type u_4<VAR>P₂ : Type u_5<VAR>Ring k<VAR>AddCommGroup V₁<VAR>Module k V₁<VAR>AffineSpace V₁ P₁<VAR>AddCommGroup V₂<VAR>Module k V₂<VAR>AffineSpace V₂ P₂<VAR>f : P₁ →ᵃ[k] P₂<GOAL>AffineSubspace.map f ⊥ = ⊥
<VAR>k : Type u_1<VAR>V₁ : Type u_2<VAR>P₁ : Type u_3<VAR>V₂ : Type u_4<VAR>P₂ : Type u_5<VAR>Ring k<VAR>AddCommGroup V₁<VAR>Module k V₁<VAR>AffineSpace V₁ P₁<VAR>AddCommGroup V₂<VAR>Module k V₂<VAR>AffineSpace V₂ P₂<VAR>f : P₁ →ᵃ[k] P₂<VAR>s : AffineSubspace k P₁<GOAL>AffineSubspace.map f 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₁<GOAL>AffineSubspace.map (AffineMap.id k P₁) s = s
<VAR>k : Type u_1<VAR>V₁ : Type u_2<VAR>P₁ : Type u_3<VAR>V₂ : Type u_4<VAR>P₂ : Type u_5<VAR>V₃ : Type u_6<VAR>P₃ : Type u_7<VAR>Ring k<VAR>AddCommGroup V₁<VAR>Module k V₁<VAR>AffineSpace V₁ P₁<VAR>AddCommGroup V₂<VAR>Module k V₂<VAR>AffineSpace V₂ P₂<VAR>AddCommGroup V₃<VAR>Module k V₃<VAR>AffineSpace V₃ P₃<VAR>s : AffineSubspace k P₁<VAR>f : P₁ →ᵃ[k] P₂<VAR>g : P₂ →ᵃ[k] P₃<GOAL>AffineSubspace.map g (AffineSubspace.map f s) = AffineSubspace.map (g.comp f) s
<VAR>k : Type u_1<VAR>V₁ : Type u_2<VAR>P₁ : Type u_3<VAR>V₂ : Type u_4<VAR>P₂ : Type u_5<VAR>Ring k<VAR>AddCommGroup V₁<VAR>Module k V₁<VAR>AffineSpace V₁ P₁<VAR>AddCommGroup V₂<VAR>Module k V₂<VAR>AffineSpace V₂ P₂<VAR>f : P₁ →ᵃ[k] P₂<VAR>s : AffineSubspace k P₁<GOAL>(AffineSubspace.map f s).direction = Submodule.map f.linear s.direction
<VAR>k : Type u_1<VAR>V₁ : Type u_2<VAR>P₁ : Type u_3<VAR>V₂ : Type u_4<VAR>P₂ : Type u_5<VAR>Ring k<VAR>AddCommGroup V₁<VAR>Module k V₁<VAR>AffineSpace V₁ P₁<VAR>AddCommGroup V₂<VAR>Module k V₂<VAR>AffineSpace V₂ P₂<VAR>f : P₁ →ᵃ[k] P₂<VAR>s : Set P₁<GOAL>AffineSubspace.map f (affineSpan k s) = affineSpan k (⇑f '' 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₂ : AffineSubspace k P₁<VAR>Nonempty ↥S₁<VAR>Nonempty ↥S₂<VAR>h : S₁ ≤ S₂<GOAL>(AffineSubspace.inclusion h).linear = Submodule.inclusion ⋯
<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₂ : AffineSubspace k P₁<VAR>Nonempty ↥S₁<VAR>Nonempty ↥S₂<VAR>h : S₁ ≤ S₂<VAR>x : ↥S₁<GOAL>↑((AffineSubspace.inclusion h) 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>S₁ : AffineSubspace k P₁<VAR>Nonempty ↥S₁<GOAL>AffineSubspace.inclusion ⋯ = AffineMap.id k ↥S₁
<VAR>k : Type u_1<VAR>V₁ : Type u_2<VAR>P₁ : Type u_3<VAR>V₂ : Type u_4<VAR>P₂ : Type u_5<VAR>Ring k<VAR>AddCommGroup V₁<VAR>Module k V₁<VAR>AffineSpace V₁ P₁<VAR>AddCommGroup V₂<VAR>Module k V₂<VAR>AffineSpace V₂ P₂<VAR>f : P₁ →ᵃ[k] P₂<VAR>hf : Function.Surjective ⇑f<GOAL>AffineSubspace.map f ⊤ = ⊤
<VAR>k : Type u_1<VAR>V₁ : Type u_2<VAR>P₁ : Type u_3<VAR>V₂ : Type u_4<VAR>P₂ : Type u_5<VAR>Ring k<VAR>AddCommGroup V₁<VAR>Module k V₁<VAR>AffineSpace V₁ P₁<VAR>AddCommGroup V₂<VAR>Module k V₂<VAR>AffineSpace V₂ P₂<VAR>f : P₁ →ᵃ[k] P₂<VAR>s : Set P₁<VAR>hf : Function.Surjective ⇑f<VAR>h : affineSpan k s = ⊤<GOAL>affineSpan k (⇑f '' 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₂ : AffineSubspace k P₁<VAR>Nonempty ↥S₁<VAR>Nonempty ↥S₂<VAR>h : S₁ = S₂<GOAL>(AffineEquiv.ofEq S₁ S₂ h).linear = LinearEquiv.ofEq S₁.direction 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₁ S₂ : AffineSubspace k P₁<VAR>Nonempty ↥S₁<VAR>Nonempty ↥S₂<VAR>h : S₁ = S₂<VAR>x : ↥S₁<GOAL>↑((AffineEquiv.ofEq S₁ S₂ h) 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>S₁ S₂ : AffineSubspace k P₁<VAR>Nonempty ↥S₁<VAR>Nonempty ↥S₂<VAR>h : S₁ = S₂<GOAL>(AffineEquiv.ofEq S₁ S₂ h).symm = AffineEquiv.ofEq 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>Nonempty ↥S₁<GOAL>AffineEquiv.ofEq S₁ S₁ ⋯ = AffineEquiv.refl k ↥S₁
<VAR>k : Type u_1<VAR>V₁ : Type u_2<VAR>P₁ : Type u_3<VAR>V₂ : Type u_4<VAR>P₂ : Type u_5<VAR>Ring k<VAR>AddCommGroup V₁<VAR>Module k V₁<VAR>AffineSpace V₁ P₁<VAR>AddCommGroup V₂<VAR>Module k V₂<VAR>AffineSpace V₂ P₂<VAR>s : Set P₁<VAR>e : P₁ ≃ᵃ[k] P₂<GOAL>affineSpan k s = ⊤ ↔ affineSpan k (⇑e '' s) = ⊤
<VAR>k : Type u_1<VAR>V₁ : Type u_2<VAR>P₁ : Type u_3<VAR>V₂ : Type u_4<VAR>P₂ : Type u_5<VAR>Ring k<VAR>AddCommGroup V₁<VAR>Module k V₁<VAR>AffineSpace V₁ P₁<VAR>AddCommGroup V₂<VAR>Module k V₂<VAR>AffineSpace V₂ P₂<VAR>f : P₁ →ᵃ[k] P₂<VAR>s : AffineSubspace k P₂<GOAL>↑(AffineSubspace.comap f s) = ⇑f ⁻¹' ↑s
<VAR>k : Type u_1<VAR>V₁ : Type u_2<VAR>P₁ : Type u_3<VAR>V₂ : Type u_4<VAR>P₂ : Type u_5<VAR>Ring k<VAR>AddCommGroup V₁<VAR>Module k V₁<VAR>AffineSpace V₁ P₁<VAR>AddCommGroup V₂<VAR>Module k V₂<VAR>AffineSpace V₂ P₂<VAR>f : P₁ →ᵃ[k] P₂<VAR>x : P₁<VAR>s : AffineSubspace k P₂<GOAL>x ∈ AffineSubspace.comap f s ↔ f x ∈ s
<VAR>k : Type u_1<VAR>V₁ : Type u_2<VAR>P₁ : Type u_3<VAR>V₂ : Type u_4<VAR>P₂ : Type u_5<VAR>Ring k<VAR>AddCommGroup V₁<VAR>Module k V₁<VAR>AffineSpace V₁ P₁<VAR>AddCommGroup V₂<VAR>Module k V₂<VAR>AffineSpace V₂ P₂<VAR>f : P₁ →ᵃ[k] P₂<VAR>s t : AffineSubspace k P₂<GOAL>s ≤ t → AffineSubspace.comap f s ≤ AffineSubspace.comap f t
<VAR>k : Type u_1<VAR>V₁ : Type u_2<VAR>P₁ : Type u_3<VAR>V₂ : Type u_4<VAR>P₂ : Type u_5<VAR>Ring k<VAR>AddCommGroup V₁<VAR>Module k V₁<VAR>AffineSpace V₁ P₁<VAR>AddCommGroup V₂<VAR>Module k V₂<VAR>AffineSpace V₂ P₂<VAR>f : P₁ →ᵃ[k] P₂<GOAL>AffineSubspace.comap f ⊤ = ⊤
<VAR>k : Type u_1<VAR>V₁ : Type u_2<VAR>P₁ : Type u_3<VAR>V₂ : Type u_4<VAR>P₂ : Type u_5<VAR>Ring k<VAR>AddCommGroup V₁<VAR>Module k V₁<VAR>AffineSpace V₁ P₁<VAR>AddCommGroup V₂<VAR>Module k V₂<VAR>AffineSpace V₂ P₂<VAR>f : P₁ →ᵃ[k] P₂<GOAL>AffineSubspace.comap 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>s : AffineSubspace k P₁<GOAL>AffineSubspace.comap (AffineMap.id k P₁) s = s
<VAR>k : Type u_1<VAR>V₁ : Type u_2<VAR>P₁ : Type u_3<VAR>V₂ : Type u_4<VAR>P₂ : Type u_5<VAR>V₃ : Type u_6<VAR>P₃ : Type u_7<VAR>Ring k<VAR>AddCommGroup V₁<VAR>Module k V₁<VAR>AffineSpace V₁ P₁<VAR>AddCommGroup V₂<VAR>Module k V₂<VAR>AffineSpace V₂ P₂<VAR>AddCommGroup V₃<VAR>Module k V₃<VAR>AffineSpace V₃ P₃<VAR>s : AffineSubspace k P₃<VAR>f : P₁ →ᵃ[k] P₂<VAR>g : P₂ →ᵃ[k] P₃<GOAL>AffineSubspace.comap f (AffineSubspace.comap g s) = AffineSubspace.comap (g.comp f) s
<VAR>k : Type u_1<VAR>V₁ : Type u_2<VAR>P₁ : Type u_3<VAR>V₂ : Type u_4<VAR>P₂ : Type u_5<VAR>Ring k<VAR>AddCommGroup V₁<VAR>Module k V₁<VAR>AffineSpace V₁ P₁<VAR>AddCommGroup V₂<VAR>Module k V₂<VAR>AffineSpace V₂ P₂<VAR>f : P₁ →ᵃ[k] P₂<VAR>s : AffineSubspace k P₁<VAR>t : AffineSubspace k P₂<GOAL>AffineSubspace.map f s ≤ t ↔ s ≤ AffineSubspace.comap f t
<VAR>k : Type u_1<VAR>V₁ : Type u_2<VAR>P₁ : Type u_3<VAR>V₂ : Type u_4<VAR>P₂ : Type u_5<VAR>Ring k<VAR>AddCommGroup V₁<VAR>Module k V₁<VAR>AffineSpace V₁ P₁<VAR>AddCommGroup V₂<VAR>Module k V₂<VAR>AffineSpace V₂ P₂<VAR>f : P₁ →ᵃ[k] P₂<GOAL>GaloisConnection (AffineSubspace.map f) (AffineSubspace.comap f)
<VAR>k : Type u_1<VAR>V₁ : Type u_2<VAR>P₁ : Type u_3<VAR>V₂ : Type u_4<VAR>P₂ : Type u_5<VAR>Ring k<VAR>AddCommGroup V₁<VAR>Module k V₁<VAR>AffineSpace V₁ P₁<VAR>AddCommGroup V₂<VAR>Module k V₂<VAR>AffineSpace V₂ P₂<VAR>f : P₁ →ᵃ[k] P₂<VAR>s : AffineSubspace k P₂<GOAL>AffineSubspace.map f (AffineSubspace.comap f s) ≤ s
<VAR>k : Type u_1<VAR>V₁ : Type u_2<VAR>P₁ : Type u_3<VAR>V₂ : Type u_4<VAR>P₂ : Type u_5<VAR>Ring k<VAR>AddCommGroup V₁<VAR>Module k V₁<VAR>AffineSpace V₁ P₁<VAR>AddCommGroup V₂<VAR>Module k V₂<VAR>AffineSpace V₂ P₂<VAR>f : P₁ →ᵃ[k] P₂<VAR>s : AffineSubspace k P₁<GOAL>s ≤ AffineSubspace.comap f (AffineSubspace.map f s)
<VAR>k : Type u_1<VAR>V₁ : Type u_2<VAR>P₁ : Type u_3<VAR>V₂ : Type u_4<VAR>P₂ : Type u_5<VAR>Ring k<VAR>AddCommGroup V₁<VAR>Module k V₁<VAR>AffineSpace V₁ P₁<VAR>AddCommGroup V₂<VAR>Module k V₂<VAR>AffineSpace V₂ P₂<VAR>s t : AffineSubspace k P₁<VAR>f : P₁ →ᵃ[k] P₂<GOAL>AffineSubspace.map f (s ⊔ t) = AffineSubspace.map f s ⊔ AffineSubspace.map f t
<VAR>k : Type u_1<VAR>V₁ : Type u_2<VAR>P₁ : Type u_3<VAR>V₂ : Type u_4<VAR>P₂ : Type u_5<VAR>Ring k<VAR>AddCommGroup V₁<VAR>Module k V₁<VAR>AffineSpace V₁ P₁<VAR>AddCommGroup V₂<VAR>Module k V₂<VAR>AffineSpace V₂ P₂<VAR>ι : Sort u_8<VAR>f : P₁ →ᵃ[k] P₂<VAR>s : ι → AffineSubspace k P₁<GOAL>AffineSubspace.map f (iSup s) = ⨆ i, AffineSubspace.map f (s i)
<VAR>k : Type u_1<VAR>V₁ : Type u_2<VAR>P₁ : Type u_3<VAR>V₂ : Type u_4<VAR>P₂ : Type u_5<VAR>Ring k<VAR>AddCommGroup V₁<VAR>Module k V₁<VAR>AffineSpace V₁ P₁<VAR>AddCommGroup V₂<VAR>Module k V₂<VAR>AffineSpace V₂ P₂<VAR>s t : AffineSubspace k P₂<VAR>f : P₁ →ᵃ[k] P₂<GOAL>AffineSubspace.comap f (s ⊓ t) = AffineSubspace.comap f s ⊓ AffineSubspace.comap f t
<VAR>k : Type u_1<VAR>V₁ : Type u_2<VAR>P₁ : Type u_3<VAR>V₂ : Type u_4<VAR>P₂ : Type u_5<VAR>Ring k<VAR>AddCommGroup V₁<VAR>Module k V₁<VAR>AffineSpace V₁ P₁<VAR>AddCommGroup V₂<VAR>Module k V₂<VAR>AffineSpace V₂ P₂<VAR>ι : Sort u_8<VAR>f : P₁ →ᵃ[k] P₂<VAR>s : ι → AffineSubspace k P₂<GOAL>AffineSubspace.comap f (iInf s) = ⨅ i, AffineSubspace.comap f (s i)
<VAR>k : Type u_1<VAR>V₁ : Type u_2<VAR>P₁ : Type u_3<VAR>V₂ : Type u_4<VAR>P₂ : Type u_5<VAR>Ring k<VAR>AddCommGroup V₁<VAR>Module k V₁<VAR>AffineSpace V₁ P₁<VAR>AddCommGroup V₂<VAR>Module k V₂<VAR>AffineSpace V₂ P₂<VAR>e : P₁ ≃ᵃ[k] P₂<VAR>s : AffineSubspace k P₁<GOAL>AffineSubspace.comap (↑e.symm) s = AffineSubspace.map (↑e) s
<VAR>k : Type u_1<VAR>V₁ : Type u_2<VAR>P₁ : Type u_3<VAR>V₂ : Type u_4<VAR>P₂ : Type u_5<VAR>Ring k<VAR>AddCommGroup V₁<VAR>Module k V₁<VAR>AffineSpace V₁ P₁<VAR>AddCommGroup V₂<VAR>Module k V₂<VAR>AffineSpace V₂ P₂<VAR>e : P₁ ≃ᵃ[k] P₂<VAR>s : AffineSubspace k P₂<GOAL>AffineSubspace.map (↑e.symm) s = AffineSubspace.comap (↑e) s
<VAR>k : Type u_1<VAR>V₁ : Type u_2<VAR>P₁ : Type u_3<VAR>V₂ : Type u_4<VAR>P₂ : Type u_5<VAR>Ring k<VAR>AddCommGroup V₁<VAR>Module k V₁<VAR>AffineSpace V₁ P₁<VAR>AddCommGroup V₂<VAR>Module k V₂<VAR>AffineSpace V₂ P₂<VAR>f : P₁ ≃ᵃ[k] P₂<VAR>s : Set P₂<GOAL>AffineSubspace.comap (↑f) (affineSpan k s) = affineSpan k (⇑f ⁻¹' 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₂ : AffineSubspace k P<VAR>h : s₁ ∥ s₂<GOAL>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₂ : AffineSubspace k P<GOAL>s₁ ∥ s₂ ↔ 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<GOAL>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₂ s₃ : AffineSubspace k P<VAR>h₁₂ : s₁ ∥ s₂<VAR>h₂₃ : s₂ ∥ s₃<GOAL>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₂ : AffineSubspace k P<VAR>h : s₁ ∥ s₂<GOAL>s₁.direction = 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<GOAL>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<GOAL>⊥ ∥ 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₂ : AffineSubspace k P<GOAL>s₁ ∥ s₂ ↔ s₁.direction = 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₁ s₂ : Set P<VAR>h : affineSpan k s₁ ∥ affineSpan k 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<VAR>s₁ s₂ : Set P<GOAL>affineSpan k s₁ ∥ affineSpan k s₂ ↔ vectorSpan k s₁ = vectorSpan k s₂ ∧ (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>p₁ p₂ p₃ p₄ : P<GOAL>affineSpan k {p₁, p₂} ∥ affineSpan k {p₃, p₄} ↔ vectorSpan k {p₁, p₂} = vectorSpan k {p₃, p₄}
<VAR>n : Type u<VAR>DecidableEq n<VAR>Fintype n<VAR>R : Type v<VAR>CommRing R<VAR>A : GL n R<GOAL>↑(Matrix.GeneralLinearGroup.det A)⁻¹ = (↑A⁻¹).det
<VAR>n : Type u<VAR>DecidableEq n<VAR>Fintype n<VAR>R : Type v<VAR>CommRing R<VAR>A : GL n R<GOAL>↑(Matrix.GeneralLinearGroup.det A) = (↑A).det
<VAR>n : Type u<VAR>DecidableEq n<VAR>Fintype n<VAR>R : Type v<VAR>CommRing R<VAR>A B : GL n R<GOAL>A = B ↔ ∀ (i j : n), ↑A i j = ↑B i j
<VAR>n : Type u<VAR>DecidableEq n<VAR>Fintype n<VAR>R : Type v<VAR>CommRing R<VAR>A B : GL n R<VAR>h : ∀ (i j : n), ↑A i j = ↑B i j<GOAL>A = B
<VAR>n : Type u<VAR>DecidableEq n<VAR>Fintype n<VAR>R : Type v<VAR>CommRing R<VAR>A B : GL n R<GOAL>↑(A * B) = ↑A * ↑B
<VAR>n : Type u<VAR>DecidableEq n<VAR>Fintype n<VAR>R : Type v<VAR>CommRing R<GOAL>↑1 = 1
<VAR>n : Type u<VAR>DecidableEq n<VAR>Fintype n<VAR>R : Type v<VAR>CommRing R<VAR>A : GL n R<GOAL>↑A⁻¹ = (↑A)⁻¹
<VAR>n : Type u<VAR>DecidableEq n<VAR>Fintype n<VAR>R : Type v<VAR>CommRing R<VAR>A : GL n R<GOAL>↑(Matrix.GeneralLinearGroup.toLinear A) = (↑A).mulVecLin
<VAR>n : Type u<VAR>DecidableEq n<VAR>Fintype n<VAR>R : Type v<VAR>CommRing R<VAR>A : GL n R<VAR>v : n → R<GOAL>(Matrix.GeneralLinearGroup.toLinear A).toLinearEquiv v = (↑A).mulVecLin v
<VAR>n : Type u<VAR>DecidableEq n<VAR>Fintype n<VAR>R : Type v<VAR>CommRing R<GOAL>Matrix.GeneralLinearGroup.map (RingHom.id R) = MonoidHom.id (GL n R)
<VAR>n : Type u<VAR>DecidableEq n<VAR>Fintype n<VAR>R : Type v<VAR>CommRing R<VAR>S : Type u_1<VAR>T : Type u_2<VAR>CommRing S<VAR>CommRing T<VAR>f : T →+* R<VAR>g : R →+* S<GOAL>Matrix.GeneralLinearGroup.map (g.comp f) = (Matrix.GeneralLinearGroup.map g).comp (Matrix.GeneralLinearGroup.map f)
<VAR>n : Type u<VAR>DecidableEq n<VAR>Fintype n<VAR>R : Type v<VAR>CommRing R<VAR>S : Type u_1<VAR>T : Type u_2<VAR>CommRing S<VAR>CommRing T<VAR>f : T →+* R<VAR>g : R →+* S<VAR>x : GL n T<GOAL>((Matrix.GeneralLinearGroup.map g).comp (Matrix.GeneralLinearGroup.map f)) x = (Matrix.GeneralLinearGroup.map g) ((Matrix.GeneralLinearGroup.map f) x)
<VAR>n : Type u<VAR>DecidableEq n<VAR>Fintype n<VAR>R : Type v<VAR>CommRing R<VAR>g : Matrix.SpecialLinearGroup n R<GOAL>Matrix.GeneralLinearGroup.det ↑g = 1
<VAR>n : Type u<VAR>R : Type v<VAR>DecidableEq n<VAR>Fintype n<VAR>LinearOrderedCommRing R<VAR>A : GL n R<GOAL>A ∈ Matrix.GLPos n R ↔ 0 < ↑(Matrix.GeneralLinearGroup.det A)
<VAR>n : Type u<VAR>R : Type v<VAR>DecidableEq n<VAR>Fintype n<VAR>LinearOrderedCommRing R<VAR>A : ↥(Matrix.GLPos n R)<GOAL>(↑↑A).det ≠ 0
<VAR>n : Type u<VAR>R : Type v<VAR>DecidableEq n<VAR>Fintype n<VAR>LinearOrderedCommRing R<VAR>Fact (Even (Fintype.card n))<VAR>g : ↥(Matrix.GLPos n R)<GOAL>↑(-g) = -↑g
<VAR>n : Type u<VAR>R : Type v<VAR>DecidableEq n<VAR>Fintype n<VAR>LinearOrderedCommRing R<VAR>Fact (Even (Fintype.card n))<VAR>g : ↥(Matrix.GLPos n R)<GOAL>↑↑(-g) = -↑↑g
<VAR>n : Type u<VAR>R : Type v<VAR>DecidableEq n<VAR>Fintype n<VAR>LinearOrderedCommRing R<VAR>Fact (Even (Fintype.card n))<VAR>g : ↥(Matrix.GLPos n R)<VAR>i j : n<GOAL>↑↑(-g) i j = -↑↑g i j
<VAR>n : Type u<VAR>DecidableEq n<VAR>Fintype n<VAR>R : Type v<VAR>LinearOrderedCommRing R<GOAL>Function.Injective ⇑Matrix.SpecialLinearGroup.toGLPos
<VAR>n : Type u<VAR>DecidableEq n<VAR>Fintype n<VAR>R : Type v<VAR>LinearOrderedCommRing R<VAR>g : Matrix.SpecialLinearGroup n R<GOAL>↑↑(Matrix.SpecialLinearGroup.toGLPos g) = ↑g
<VAR>n : Type u<VAR>DecidableEq n<VAR>Fintype n<VAR>R : Type v<VAR>LinearOrderedCommRing R<VAR>g : Matrix.SpecialLinearGroup n R<GOAL>Matrix.GeneralLinearGroup.det ↑(Matrix.SpecialLinearGroup.toGLPos g) = 1
<VAR>n : Type u<VAR>DecidableEq n<VAR>Fintype n<VAR>R : Type v<VAR>LinearOrderedCommRing R<VAR>Fact (Even (Fintype.card n))<VAR>g : Matrix.SpecialLinearGroup n R<GOAL>Matrix.SpecialLinearGroup.toGLPos (-g) = -Matrix.SpecialLinearGroup.toGLPos g
<VAR>𝕜 : Type u_1<VAR>RCLike 𝕜<VAR>n : Type u_2<VAR>LinearOrder n<VAR>IsWellOrder n fun x x_1 => x < x_1<VAR>LocallyFiniteOrderBot n<VAR>S : Matrix n n 𝕜<VAR>Fintype n<VAR>hS : S.PosDef<GOAL>LDL.lowerInv hS = ((Pi.basisFun 𝕜 n).toMatrix ⇑(gramSchmidtBasis (Pi.basisFun 𝕜 n))).transpose
<VAR>𝕜 : Type u_1<VAR>RCLike 𝕜<VAR>n : Type u_2<VAR>LinearOrder n<VAR>IsWellOrder n fun x x_1 => x < x_1<VAR>LocallyFiniteOrderBot n<VAR>S : Matrix n n 𝕜<VAR>Fintype n<VAR>hS : S.PosDef<VAR>i j : n<VAR>h₀ : i ≠ j<GOAL>⟪(WithLp.equiv 2 (n → 𝕜)).symm (LDL.lowerInv hS i), (WithLp.equiv 2 (n → 𝕜)).symm (S.transpose.mulVec (LDL.lowerInv hS j))⟫_𝕜 = 0
<VAR>𝕜 : Type u_1<VAR>RCLike 𝕜<VAR>n : Type u_2<VAR>LinearOrder n<VAR>IsWellOrder n fun x x_1 => x < x_1<VAR>LocallyFiniteOrderBot n<VAR>S : Matrix n n 𝕜<VAR>Fintype n<VAR>hS : S.PosDef<VAR>i j : n<VAR>hij : i < j<GOAL>LDL.lowerInv hS i j = 0
<VAR>𝕜 : Type u_1<VAR>RCLike 𝕜<VAR>n : Type u_2<VAR>LinearOrder n<VAR>IsWellOrder n fun x x_1 => x < x_1<VAR>LocallyFiniteOrderBot n<VAR>S : Matrix n n 𝕜<VAR>Fintype n<VAR>hS : S.PosDef<GOAL>LDL.diag hS = LDL.lowerInv hS * S * (LDL.lowerInv hS).conjTranspose
<VAR>𝕜 : Type u_1<VAR>RCLike 𝕜<VAR>n : Type u_2<VAR>LinearOrder n<VAR>IsWellOrder n fun x x_1 => x < x_1<VAR>LocallyFiniteOrderBot n<VAR>S : Matrix n n 𝕜<VAR>Fintype n<VAR>hS : S.PosDef<GOAL>LDL.lower hS * LDL.diag hS * (LDL.lower hS).conjTranspose = S
<VAR>R₂ : Type u_5<VAR>CommSemiring R₂<VAR>n : Type u_11<VAR>Fintype n<VAR>DecidableEq n<VAR>M : Matrix n n R₂<VAR>i j : n<GOAL>(M.toBilin'Aux ((LinearMap.stdBasis R₂ (fun x => R₂) i) 1)) ((LinearMap.stdBasis R₂ (fun x => R₂) j) 1) = M i 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>B : LinearMap.BilinForm R₂ M₂<VAR>b : n → M₂<VAR>i j : n<GOAL>(BilinForm.toMatrixAux b) B i j = (B (b i)) (b j)
<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₂)<GOAL>((BilinForm.toMatrixAux fun j => (LinearMap.stdBasis R₂ (fun x => R₂) j) 1) B₂).toBilin'Aux = B₂
<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₂)<GOAL>(BilinForm.toMatrixAux fun j => (LinearMap.stdBasis R₂ (fun x => R₂) j) 1) B = LinearMap.BilinForm.toMatrix' B
<VAR>R₂ : Type u_5<VAR>CommSemiring R₂<VAR>n : Type u_11<VAR>Fintype n<VAR>DecidableEq n<VAR>M : Matrix n n R₂<GOAL>M.toBilin'Aux = Matrix.toBilin' M
<VAR>R₂ : Type u_5<VAR>CommSemiring R₂<VAR>n : Type u_11<VAR>Fintype n<VAR>DecidableEq n<VAR>M : Matrix n n R₂<VAR>x y : n → R₂<GOAL>((Matrix.toBilin' M) x) y = ∑ i : n, ∑ j : n, x i * M i j * y j
<VAR>R₂ : Type u_5<VAR>CommSemiring R₂<VAR>n : Type u_11<VAR>Fintype n<VAR>DecidableEq n<VAR>M : Matrix n n R₂<VAR>v w : n → R₂<GOAL>((Matrix.toBilin' M) v) w = Matrix.dotProduct v (M.mulVec w)
<VAR>R₂ : Type u_5<VAR>CommSemiring R₂<VAR>n : Type u_11<VAR>Fintype n<VAR>DecidableEq n<VAR>M : Matrix n n R₂<VAR>i j : n<GOAL>((Matrix.toBilin' M) ((LinearMap.stdBasis R₂ (fun x => R₂) i) 1)) ((LinearMap.stdBasis R₂ (fun x => R₂) j) 1) = M i j
<VAR>R₂ : Type u_5<VAR>CommSemiring R₂<VAR>n : Type u_11<VAR>Fintype n<VAR>DecidableEq n<GOAL>LinearMap.BilinForm.toMatrix'.symm = Matrix.toBilin'
<VAR>R₂ : Type u_5<VAR>CommSemiring R₂<VAR>n : Type u_11<VAR>Fintype n<VAR>DecidableEq n<GOAL>Matrix.toBilin'.symm = LinearMap.BilinForm.toMatrix'
<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₂)<GOAL>Matrix.toBilin' (LinearMap.BilinForm.toMatrix' B) = B
<VAR>R₂ : Type u_5<VAR>CommSemiring R₂<VAR>n : Type u_11<VAR>Fintype n<VAR>DecidableEq n<VAR>M : Matrix n n R₂<GOAL>LinearMap.BilinForm.toMatrix' (Matrix.toBilin' M) = M
<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>i j : n<GOAL>LinearMap.BilinForm.toMatrix' B i j = (B ((LinearMap.stdBasis R₂ (fun x => R₂) i) 1)) ((LinearMap.stdBasis R₂ (fun x => R₂) j) 1)
<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>B : LinearMap.BilinForm R₂ (n → R₂)<VAR>l r : (o → R₂) →ₗ[R₂] n → R₂<GOAL>LinearMap.BilinForm.toMatrix' (B.comp l r) = (LinearMap.toMatrix' l).transpose * LinearMap.BilinForm.toMatrix' B * LinearMap.toMatrix' r
<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>f : (n → R₂) →ₗ[R₂] n → R₂<GOAL>LinearMap.BilinForm.toMatrix' (B.compLeft f) = (LinearMap.toMatrix' f).transpose * LinearMap.BilinForm.toMatrix' B
<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>f : (n → R₂) →ₗ[R₂] n → R₂<GOAL>LinearMap.BilinForm.toMatrix' (B.compRight f) = LinearMap.BilinForm.toMatrix' B * LinearMap.toMatrix' f
<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>B : LinearMap.BilinForm R₂ (n → R₂)<VAR>M : Matrix o n R₂<VAR>N : Matrix n o R₂<GOAL>M * LinearMap.BilinForm.toMatrix' B * N = LinearMap.BilinForm.toMatrix' (B.comp (Matrix.toLin' M.transpose) (Matrix.toLin' N))