ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>M : Type u_5<VAR>M₁ : Type u_6<VAR>M₃ : Type u_8<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>AddCommMonoid M₁<VAR>Module R M₁<VAR>AddCommMonoid M₃<VAR>Module R M₃<VAR>I : R →+* R<VAR>B : M →ₗ[R] M →ₛₗ[I] M₃<VAR>B' : M₁ →ₗ[R] M₁ →ₛₗ[I] M₃<VAR>f : M →ₗ[R] M₁<VAR>g : M₁ →ₗ[R] M<GOAL>B.IsAdjointPair B' f g ↔ B' ∘ₗ f = B.compl₂ g
<VAR>R : Type u_1<VAR>M : Type u_5<VAR>M₁ : Type u_6<VAR>M₃ : Type u_8<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>AddCommMonoid M₁<VAR>Module R M₁<VAR>AddCommMonoid M₃<VAR>Module R M₃<VAR>I : R →+* R<VAR>B : M →ₗ[R] M →ₛₗ[I] M₃<VAR>B' : M₁ →ₗ[R] M₁ →ₛₗ[I] M₃<GOAL>B.IsAdjointPair B' 0 0
<VAR>R : Type u_1<VAR>M : Type u_5<VAR>M₃ : Type u_8<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>AddCommMonoid M₃<VAR>Module R M₃<VAR>I : R →+* R<VAR>B : M →ₗ[R] M →ₛₗ[I] M₃<GOAL>B.IsAdjointPair B 1 1
<VAR>R : Type u_1<VAR>M : Type u_5<VAR>M₁ : Type u_6<VAR>M₃ : Type u_8<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>AddCommMonoid M₁<VAR>Module R M₁<VAR>AddCommMonoid M₃<VAR>Module R M₃<VAR>I : R →+* R<VAR>B : M →ₗ[R] M →ₛₗ[I] M₃<VAR>B' : M₁ →ₗ[R] M₁ →ₛₗ[I] M₃<VAR>f f' : M →ₗ[R] M₁<VAR>g g' : M₁ →ₗ[R] M<VAR>h : B.IsAdjointPair B' f g<VAR>h' : B.IsAdjointPair B' f' g'<GOAL>B.IsAdjointPair B' (f + f') (g + g')
<VAR>R : Type u_1<VAR>M : Type u_5<VAR>M₁ : Type u_6<VAR>M₂ : Type u_7<VAR>M₃ : Type u_8<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>AddCommMonoid M₁<VAR>Module R M₁<VAR>AddCommMonoid M₂<VAR>Module R M₂<VAR>AddCommMonoid M₃<VAR>Module R M₃<VAR>I : R →+* R<VAR>B : M →ₗ[R] M →ₛₗ[I] M₃<VAR>B' : M₁ →ₗ[R] M₁ →ₛₗ[I] M₃<VAR>B'' : M₂ →ₗ[R] M₂ →ₛₗ[I] M₃<VAR>f : M →ₗ[R] M₁<VAR>g : M₁ →ₗ[R] M<VAR>f' : M₁ →ₗ[R] M₂<VAR>g' : M₂ →ₗ[R] M₁<VAR>h : B.IsAdjointPair B' f g<VAR>h' : B'.IsAdjointPair B'' f' g'<GOAL>B.IsAdjointPair B'' (f' ∘ₗ f) (g ∘ₗ g')
<VAR>R : Type u_1<VAR>M : Type u_5<VAR>M₃ : Type u_8<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>AddCommMonoid M₃<VAR>Module R M₃<VAR>I : R →+* R<VAR>B : M →ₗ[R] M →ₛₗ[I] M₃<VAR>f g f' g' : Module.End R M<VAR>h : B.IsAdjointPair B f g<VAR>h' : B.IsAdjointPair B f' g'<GOAL>B.IsAdjointPair B (f * f') (g' * g)
<VAR>R : Type u_1<VAR>M : Type u_5<VAR>M₁ : Type u_6<VAR>M₂ : Type u_7<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>AddCommGroup M₁<VAR>Module R M₁<VAR>AddCommGroup M₂<VAR>Module R M₂<VAR>B : M →ₗ[R] M →ₗ[R] M₂<VAR>B' : M₁ →ₗ[R] M₁ →ₗ[R] M₂<VAR>f f' : M →ₗ[R] M₁<VAR>g g' : M₁ →ₗ[R] M<VAR>h : B.IsAdjointPair B' f g<VAR>h' : B.IsAdjointPair B' f' g'<GOAL>B.IsAdjointPair B' (f - f') (g - g')
<VAR>R : Type u_1<VAR>M : Type u_5<VAR>M₁ : Type u_6<VAR>M₂ : Type u_7<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>AddCommGroup M₁<VAR>Module R M₁<VAR>AddCommGroup M₂<VAR>Module R M₂<VAR>B : M →ₗ[R] M →ₗ[R] M₂<VAR>B' : M₁ →ₗ[R] M₁ →ₗ[R] M₂<VAR>f : M →ₗ[R] M₁<VAR>g : M₁ →ₗ[R] M<VAR>c : R<VAR>h : B.IsAdjointPair B' f g<GOAL>B.IsAdjointPair B' (c • f) (c • g)
<VAR>R : Type u_1<VAR>M : Type u_5<VAR>M₂ : Type u_7<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>AddCommGroup M₂<VAR>Module R M₂<VAR>B F : M →ₗ[R] M →ₗ[R] M₂<VAR>f : Module.End R M<GOAL>f ∈ B.isPairSelfAdjointSubmodule F ↔ B.IsPairSelfAdjoint F f
<VAR>R : Type u_1<VAR>M : Type u_5<VAR>M₁ : Type u_6<VAR>M₂ : Type u_7<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>AddCommGroup M₁<VAR>Module R M₁<VAR>AddCommGroup M₂<VAR>Module R M₂<VAR>B F : M →ₗ[R] M →ₗ[R] M₂<VAR>e : M₁ ≃ₗ[R] M<VAR>f : Module.End R M<GOAL>B.IsPairSelfAdjoint F f ↔ (B.compl₁₂ ↑e ↑e).IsPairSelfAdjoint (F.compl₁₂ ↑e ↑e) (e.symm.conj f)
<VAR>R : Type u_1<VAR>M : Type u_5<VAR>M₂ : Type u_7<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>AddCommGroup M₂<VAR>Module R M₂<VAR>B : M →ₗ[R] M →ₗ[R] M₂<VAR>f : Module.End R M<GOAL>B.IsSkewAdjoint f ↔ (-B).IsAdjointPair B f f
<VAR>R : Type u_1<VAR>M : Type u_5<VAR>M₂ : Type u_7<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>AddCommGroup M₂<VAR>Module R M₂<VAR>B : M →ₗ[R] M →ₗ[R] M₂<VAR>f : Module.End R M<GOAL>f ∈ B.selfAdjointSubmodule ↔ B.IsSelfAdjoint f
<VAR>R : Type u_1<VAR>M : Type u_5<VAR>M₂ : Type u_7<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>AddCommGroup M₂<VAR>Module R M₂<VAR>B : M →ₗ[R] M →ₗ[R] M₂<VAR>f : Module.End R M<GOAL>f ∈ B.skewAdjointSubmodule ↔ B.IsSkewAdjoint f
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>M : Type u_5<VAR>M₁ : Type u_6<VAR>M₂ : Type u_7<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>CommSemiring R₁<VAR>AddCommMonoid M₁<VAR>Module R₁ M₁<VAR>CommSemiring R₂<VAR>AddCommMonoid M₂<VAR>Module R₂ M₂<VAR>I₁ : R₁ →+* R<VAR>I₂ : R₂ →+* R<VAR>Nontrivial M₁<GOAL>¬LinearMap.SeparatingLeft 0
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>M : Type u_5<VAR>M₁ : Type u_6<VAR>M₂ : Type u_7<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>CommSemiring R₁<VAR>AddCommMonoid M₁<VAR>Module R₁ M₁<VAR>CommSemiring R₂<VAR>AddCommMonoid M₂<VAR>Module R₂ M₂<VAR>I₁ : R₁ →+* R<VAR>I₂ : R₂ →+* R<VAR>Nontrivial M₁<VAR>B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] M<VAR>h : B.SeparatingLeft<GOAL>B ≠ 0
<VAR>R : Type u_1<VAR>M : Type u_5<VAR>Mₗ₁ : Type u_9<VAR>Mₗ₁' : Type u_10<VAR>Mₗ₂ : Type u_11<VAR>Mₗ₂' : Type u_12<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>AddCommMonoid Mₗ₁<VAR>AddCommMonoid Mₗ₂<VAR>AddCommMonoid Mₗ₁'<VAR>AddCommMonoid Mₗ₂'<VAR>Module R Mₗ₁<VAR>Module R Mₗ₂<VAR>Module R Mₗ₁'<VAR>Module R Mₗ₂'<VAR>B : Mₗ₁ →ₗ[R] Mₗ₂ →ₗ[R] M<VAR>e₁ : Mₗ₁ ≃ₗ[R] Mₗ₁'<VAR>e₂ : Mₗ₂ ≃ₗ[R] Mₗ₂'<VAR>h : B.SeparatingLeft<GOAL>((e₁.arrowCongr (e₂.arrowCongr (LinearEquiv.refl R M))) B).SeparatingLeft
<VAR>R : Type u_1<VAR>M : Type u_5<VAR>Mₗ₁ : Type u_9<VAR>Mₗ₁' : Type u_10<VAR>Mₗ₂ : Type u_11<VAR>Mₗ₂' : Type u_12<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>AddCommMonoid Mₗ₁<VAR>AddCommMonoid Mₗ₂<VAR>AddCommMonoid Mₗ₁'<VAR>AddCommMonoid Mₗ₂'<VAR>Module R Mₗ₁<VAR>Module R Mₗ₂<VAR>Module R Mₗ₁'<VAR>Module R Mₗ₂'<VAR>B : Mₗ₁ →ₗ[R] Mₗ₂ →ₗ[R] M<VAR>e₁ : Mₗ₁ ≃ₗ[R] Mₗ₁'<VAR>e₂ : Mₗ₂ ≃ₗ[R] Mₗ₂'<GOAL>((e₁.arrowCongr (e₂.arrowCongr (LinearEquiv.refl R M))) B).SeparatingLeft ↔ B.SeparatingLeft
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>M : Type u_5<VAR>M₁ : Type u_6<VAR>M₂ : Type u_7<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>CommSemiring R₁<VAR>AddCommMonoid M₁<VAR>Module R₁ M₁<VAR>CommSemiring R₂<VAR>AddCommMonoid M₂<VAR>Module R₂ M₂<VAR>I₁ : R₁ →+* R<VAR>I₂ : R₂ →+* R<VAR>B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] M<GOAL>B.flip.SeparatingRight ↔ B.SeparatingLeft
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>M : Type u_5<VAR>M₁ : Type u_6<VAR>M₂ : Type u_7<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>CommSemiring R₁<VAR>AddCommMonoid M₁<VAR>Module R₁ M₁<VAR>CommSemiring R₂<VAR>AddCommMonoid M₂<VAR>Module R₂ M₂<VAR>I₁ : R₁ →+* R<VAR>I₂ : R₂ →+* R<VAR>B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] M<GOAL>B.flip.SeparatingLeft ↔ B.SeparatingRight
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>M : Type u_5<VAR>M₁ : Type u_6<VAR>M₂ : Type u_7<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>CommSemiring R₁<VAR>AddCommMonoid M₁<VAR>Module R₁ M₁<VAR>CommSemiring R₂<VAR>AddCommMonoid M₂<VAR>Module R₂ M₂<VAR>I₁ : R₁ →+* R<VAR>I₂ : R₂ →+* R<VAR>B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] M<GOAL>B.flip.Nondegenerate ↔ B.Nondegenerate
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>M : Type u_5<VAR>M₁ : Type u_6<VAR>M₂ : Type u_7<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>CommSemiring R₁<VAR>AddCommMonoid M₁<VAR>Module R₁ M₁<VAR>CommSemiring R₂<VAR>AddCommMonoid M₂<VAR>Module R₂ M₂<VAR>I₁ : R₁ →+* R<VAR>I₂ : R₂ →+* R<VAR>B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] M<GOAL>B.SeparatingLeft ↔ ∀ (x : M₁), B x = 0 → x = 0
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>M : Type u_5<VAR>M₁ : Type u_6<VAR>M₂ : Type u_7<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>CommSemiring R₁<VAR>AddCommMonoid M₁<VAR>Module R₁ M₁<VAR>CommSemiring R₂<VAR>AddCommMonoid M₂<VAR>Module R₂ M₂<VAR>I₁ : R₁ →+* R<VAR>I₂ : R₂ →+* R<VAR>B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] M<GOAL>B.SeparatingRight ↔ ∀ (y : M₂), B.flip y = 0 → y = 0
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>M : Type u_5<VAR>M₁ : Type u_6<VAR>M₂ : Type u_7<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>CommSemiring R₁<VAR>AddCommMonoid M₁<VAR>Module R₁ M₁<VAR>CommSemiring R₂<VAR>AddCommMonoid M₂<VAR>Module R₂ M₂<VAR>I₁ : R₁ →+* R<VAR>I₂ : R₂ →+* R<VAR>B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] M<GOAL>B.SeparatingLeft ↔ LinearMap.ker B = ⊥
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>M : Type u_5<VAR>M₁ : Type u_6<VAR>M₂ : Type u_7<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>CommSemiring R₁<VAR>AddCommMonoid M₁<VAR>Module R₁ M₁<VAR>CommSemiring R₂<VAR>AddCommMonoid M₂<VAR>Module R₂ M₂<VAR>I₁ : R₁ →+* R<VAR>I₂ : R₂ →+* R<VAR>B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] M<GOAL>B.SeparatingRight ↔ LinearMap.ker B.flip = ⊥
<VAR>R : Type u_1<VAR>M : Type u_5<VAR>M₁ : Type u_6<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>AddCommGroup M₁<VAR>Module R M₁<VAR>B : M →ₗ[R] M →ₗ[R] M₁<VAR>hB : B.IsRefl<VAR>hB' : B.SeparatingLeft<GOAL>B.Nondegenerate
<VAR>R : Type u_1<VAR>M : Type u_5<VAR>M₁ : Type u_6<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>AddCommGroup M₁<VAR>Module R M₁<VAR>B : M →ₗ[R] M →ₗ[R] M₁<VAR>hB : B.IsRefl<VAR>hB' : B.SeparatingRight<GOAL>B.Nondegenerate
<VAR>R : Type u_1<VAR>M : Type u_5<VAR>M₁ : Type u_6<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>AddCommGroup M₁<VAR>Module R M₁<VAR>B : M →ₗ[R] M →ₗ[R] M₁<VAR>hB : B.IsRefl<VAR>W : Submodule R M<VAR>hW : Disjoint W (W.orthogonalBilin B)<GOAL>(B.domRestrict₁₂ W W).Nondegenerate
<VAR>R : Type u_1<VAR>M : Type u_5<VAR>M₁ : Type u_6<VAR>n : Type u_19<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>AddCommGroup M₁<VAR>Module R M₁<VAR>I I' : R →+* R<VAR>Nontrivial R<VAR>B : M →ₛₗ[I] M →ₛₗ[I'] M₁<VAR>v : Basis n R M<VAR>h : B.IsOrthoᵢ ⇑v<VAR>hB : B.SeparatingLeft<VAR>i : n<GOAL>¬B.IsOrtho (v i) (v i)
<VAR>R : Type u_1<VAR>M : Type u_5<VAR>M₁ : Type u_6<VAR>n : Type u_19<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>AddCommGroup M₁<VAR>Module R M₁<VAR>I I' : R →+* R<VAR>Nontrivial R<VAR>B : M →ₛₗ[I] M →ₛₗ[I'] M₁<VAR>v : Basis n R M<VAR>h : B.IsOrthoᵢ ⇑v<VAR>hB : B.SeparatingRight<VAR>i : n<GOAL>¬B.IsOrtho (v i) (v i)
<VAR>R : Type u_1<VAR>M : Type u_5<VAR>M₁ : Type u_6<VAR>n : Type u_19<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>AddCommGroup M₁<VAR>Module R M₁<VAR>NoZeroSMulDivisors R M₁<VAR>B : M →ₗ[R] M →ₗ[R] M₁<VAR>v : Basis n R M<VAR>hO : B.IsOrthoᵢ ⇑v<VAR>h : ∀ (i : n), ¬B.IsOrtho (v i) (v i)<GOAL>B.SeparatingLeft
<VAR>R : Type u_1<VAR>M : Type u_5<VAR>M₁ : Type u_6<VAR>n : Type u_19<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>AddCommGroup M₁<VAR>Module R M₁<VAR>NoZeroSMulDivisors R M₁<VAR>B : M →ₗ[R] M →ₗ[R] M₁<VAR>v : Basis n R M<VAR>hO : B.IsOrthoᵢ ⇑v<VAR>h : ∀ (i : n), ¬B.IsOrtho (v i) (v i)<GOAL>B.SeparatingRight
<VAR>R : Type u_1<VAR>M : Type u_5<VAR>M₁ : Type u_6<VAR>n : Type u_19<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>AddCommGroup M₁<VAR>Module R M₁<VAR>NoZeroSMulDivisors R M₁<VAR>B : M →ₗ[R] M →ₗ[R] M₁<VAR>v : Basis n R M<VAR>hO : B.IsOrthoᵢ ⇑v<VAR>h : ∀ (i : n), ¬B.IsOrtho (v i) (v i)<GOAL>B.Nondegenerate
<VAR>K : Type u<VAR>V : Type v<VAR>DivisionRing K<VAR>AddCommGroup V<VAR>Module K V<VAR>V₂ : Type v'<VAR>AddCommGroup V₂<VAR>Module K V₂<VAR>f : V →ₗ[K] V₂<VAR>w : Function.Injective ⇑f<VAR>FiniteDimensional K V₂<GOAL>FiniteDimensional K V
<VAR>K : Type u<VAR>V : Type v<VAR>DivisionRing K<VAR>AddCommGroup V<VAR>Module K V<VAR>V₂ : Type v'<VAR>AddCommGroup V₂<VAR>Module K V₂<VAR>f : V →ₗ[K] V₂<VAR>w : Function.Surjective ⇑f<VAR>FiniteDimensional K V<GOAL>FiniteDimensional K V₂
<VAR>K : Type u<VAR>V : Type v<VAR>DivisionRing K<VAR>AddCommGroup V<VAR>Module K V<VAR>Finite K<VAR>FiniteDimensional K V<GOAL>Finite V
<VAR>K : Type u<VAR>V : Type v<VAR>DivisionRing K<VAR>AddCommGroup V<VAR>Module K V<VAR>ι : Type w<VAR>Finite ι<VAR>h : Basis ι K V<GOAL>FiniteDimensional K V
<VAR>K : Type u<VAR>V : Type v<VAR>DivisionRing K<VAR>AddCommGroup V<VAR>Module K V<VAR>ι : Type w<VAR>s : Set ι<VAR>h : Basis (↑s) K V<VAR>hs : s.Finite<GOAL>FiniteDimensional K V
<VAR>K : Type u<VAR>V : Type v<VAR>DivisionRing K<VAR>AddCommGroup V<VAR>Module K V<VAR>FiniteDimensional K V<GOAL>↑(FiniteDimensional.finrank K V) = Module.rank K V
<VAR>K : Type u<VAR>V : Type v<VAR>DivisionRing K<VAR>AddCommGroup V<VAR>Module K V<VAR>h : ¬FiniteDimensional K V<GOAL>FiniteDimensional.finrank K V = 0
<VAR>K : Type u<VAR>V : Type v<VAR>DivisionRing K<VAR>AddCommGroup V<VAR>Module K V<VAR>h : 0 < FiniteDimensional.finrank K V<GOAL>FiniteDimensional K V
<VAR>K : Type u<VAR>V : Type v<VAR>DivisionRing K<VAR>AddCommGroup V<VAR>Module K V<VAR>n : ℕ<VAR>hn : FiniteDimensional.finrank K V = n.succ<GOAL>FiniteDimensional K V
<VAR>K : Type u<VAR>V : Type v<VAR>DivisionRing K<VAR>AddCommGroup V<VAR>Module K V<VAR>n : ℕ<VAR>hn : Fact (FiniteDimensional.finrank K V = n + 1)<GOAL>FiniteDimensional K V
<VAR>K : Type u<VAR>V : Type v<VAR>DivisionRing K<VAR>AddCommGroup V<VAR>Module K V<VAR>W : Type v<VAR>AddCommGroup W<VAR>Module K W<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>hVW : Module.rank K V = n • Module.rank K W<GOAL>FiniteDimensional K V ↔ FiniteDimensional K W
<VAR>K : Type u<VAR>V : Type v<VAR>DivisionRing K<VAR>AddCommGroup V<VAR>Module K V<VAR>FiniteDimensional K V<VAR>ι : Type w<VAR>h : Basis ι K V<GOAL>↑(FiniteDimensional.finrank K V) = #ι
<VAR>K : Type u<VAR>V : Type v<VAR>DivisionRing K<VAR>AddCommGroup V<VAR>Module K V<VAR>ι : Type w<VAR>FiniteDimensional K V<VAR>v : ι → V<VAR>h : LinearIndependent K v<GOAL>#ι < ℵ₀
<VAR>K : Type u<VAR>V : Type v<VAR>DivisionRing K<VAR>AddCommGroup V<VAR>Module K V<VAR>FiniteDimensional K V<VAR>S : Submodule K V<VAR>h : FiniteDimensional.finrank K ↥S = FiniteDimensional.finrank K V<GOAL>S = ⊤
<VAR>K : Type u<VAR>V : Type v<VAR>DivisionRing K<VAR>AddCommGroup V<VAR>Module K V<VAR>A : Set V<VAR>hA : A.Finite<GOAL>FiniteDimensional K ↥(Submodule.span K A)
<VAR>L : Type u_1<VAR>LinearOrderedField L<VAR>W : Type v<VAR>AddCommGroup W<VAR>Module L W<VAR>FiniteDimensional L W<VAR>t : Finset W<VAR>h : FiniteDimensional.finrank L W + 1 < t.card<GOAL>∃ f, ∑ e ∈ t, f e • e = 0 ∧ ∑ e ∈ t, f e = 0 ∧ ∃ x ∈ t, 0 < f x
<VAR>K : Type u<VAR>V : Type v<VAR>DivisionRing K<VAR>AddCommGroup V<VAR>Module K V<VAR>ι : Type u_1<VAR>Unique ι<VAR>h : FiniteDimensional.finrank K V = 1<VAR>v : V<VAR>hv : v ≠ 0<VAR>w : V<GOAL>(FiniteDimensional.basisSingleton ι h v hv).repr w = Finsupp.single default (((FiniteDimensional.basisUnique ι h).repr w) default / ((FiniteDimensional.basisUnique ι h).repr v) default)
<VAR>K : Type u<VAR>V : Type v<VAR>DivisionRing K<VAR>AddCommGroup V<VAR>Module K V<VAR>ι : Type u_1<VAR>Unique ι<VAR>h : FiniteDimensional.finrank K V = 1<VAR>v : V<VAR>hv : v ≠ 0<VAR>i : ι<GOAL>(FiniteDimensional.basisSingleton ι h v hv) i = v
<VAR>K : Type u<VAR>V : Type v<VAR>DivisionRing K<VAR>AddCommGroup V<VAR>Module K V<VAR>ι : Type u_1<VAR>Unique ι<VAR>h : FiniteDimensional.finrank K V = 1<VAR>v : V<VAR>hv : v ≠ 0<GOAL>Set.range ⇑(FiniteDimensional.basisSingleton ι h v hv) = {v}
<VAR>F : Type u_1<VAR>K : Type u_2<VAR>A : Type u_3<VAR>DivisionRing F<VAR>DivisionRing K<VAR>AddCommGroup A<VAR>Module F K<VAR>Module K A<VAR>Module F A<VAR>IsScalarTower F K A<VAR>FiniteDimensional F K<VAR>FiniteDimensional K A<GOAL>FiniteDimensional F A
<VAR>K : Type u<VAR>V : Type v<VAR>DivisionRing K<VAR>AddCommGroup V<VAR>Module K V<VAR>n : ℕ<VAR>h : Module.rank K V = ↑n<GOAL>FiniteDimensional K V
<VAR>K : Type u<VAR>V : Type v<VAR>DivisionRing K<VAR>AddCommGroup V<VAR>Module K V<VAR>h : Module.rank K V = 0<GOAL>FiniteDimensional K V
<VAR>K : Type u<VAR>V : Type v<VAR>DivisionRing K<VAR>AddCommGroup V<VAR>Module K V<VAR>h : Module.rank K V = 1<GOAL>FiniteDimensional K V
<VAR>K : Type u<VAR>V : Type v<VAR>DivisionRing K<VAR>AddCommGroup V<VAR>Module K V<VAR>s : Submodule K V<GOAL>s.FG ↔ FiniteDimensional K ↥s
<VAR>K : Type u<VAR>V : Type v<VAR>DivisionRing K<VAR>AddCommGroup V<VAR>Module K V<VAR>S₁ S₂ : Submodule K V<VAR>FiniteDimensional K ↥S₂<VAR>h : S₁ ≤ S₂<GOAL>FiniteDimensional K ↥S₁
<VAR>K : Type u<VAR>V : Type v<VAR>DivisionRing K<VAR>AddCommGroup V<VAR>Module K V<VAR>V₂ : Type v'<VAR>AddCommGroup V₂<VAR>Module K V₂<VAR>f : V ≃ₗ[K] V₂<VAR>FiniteDimensional K V<GOAL>FiniteDimensional K V₂
<VAR>K : Type u<VAR>V : Type v<VAR>DivisionRing K<VAR>AddCommGroup V<VAR>Module K V<VAR>S₁ S₂ : Submodule K V<VAR>FiniteDimensional K ↥S₂<VAR>hle : S₁ ≤ S₂<VAR>hd : FiniteDimensional.finrank K ↥S₂ ≤ FiniteDimensional.finrank K ↥S₁<GOAL>S₁ = S₂
<VAR>K : Type u<VAR>V : Type v<VAR>DivisionRing K<VAR>AddCommGroup V<VAR>Module K V<VAR>S₁ S₂ : Submodule K V<VAR>FiniteDimensional K ↥S₂<VAR>hle : S₁ ≤ S₂<VAR>hd : FiniteDimensional.finrank K ↥S₁ = FiniteDimensional.finrank K ↥S₂<GOAL>S₁ = S₂
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>Field K<VAR>Ring L<VAR>Algebra K L<VAR>F E : Subalgebra K L<VAR>hfin : FiniteDimensional K ↥E<VAR>h_le : F ≤ E<VAR>h_finrank : FiniteDimensional.finrank K ↥E ≤ FiniteDimensional.finrank K ↥F<GOAL>F = E
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>Field K<VAR>Ring L<VAR>Algebra K L<VAR>F E : Subalgebra K L<VAR>hfin : FiniteDimensional K ↥E<VAR>h_le : F ≤ E<VAR>h_finrank : FiniteDimensional.finrank K ↥F = FiniteDimensional.finrank K ↥E<GOAL>F = E
<VAR>K : Type u<VAR>V : Type v<VAR>DivisionRing K<VAR>AddCommGroup V<VAR>Module K V<VAR>FiniteDimensional K V<VAR>f : V →ₗ[K] V<VAR>hinj : Function.Injective ⇑f<GOAL>Function.Surjective ⇑f
<VAR>K : Type u<VAR>V : Type v<VAR>DivisionRing K<VAR>AddCommGroup V<VAR>Module K V<VAR>V₂ : Type v'<VAR>AddCommGroup V₂<VAR>Module K V₂<VAR>FiniteDimensional K V<VAR>f : V →ₗ[K] V₂<VAR>hf : LinearMap.range f = ⊤<GOAL>FiniteDimensional K V₂
<VAR>K : Type u<VAR>V : Type v<VAR>DivisionRing K<VAR>AddCommGroup V<VAR>Module K V<VAR>FiniteDimensional K V<VAR>f : V →ₗ[K] V<GOAL>Function.Injective ⇑f ↔ Function.Surjective ⇑f
<VAR>K : Type u<VAR>V : Type v<VAR>DivisionRing K<VAR>AddCommGroup V<VAR>Module K V<VAR>p : Submodule K V<VAR>FiniteDimensional K ↥p<VAR>f : V →ₗ[K] V<VAR>h : ∀ x ∈ p, f x ∈ p<GOAL>Set.InjOn ⇑f ↑p ↔ Set.SurjOn ⇑f ↑p ↑p
<VAR>K : Type u<VAR>V : Type v<VAR>DivisionRing K<VAR>AddCommGroup V<VAR>Module K V<VAR>FiniteDimensional K V<VAR>f : V →ₗ[K] V<GOAL>LinearMap.ker f = ⊥ ↔ LinearMap.range f = ⊤
<VAR>K : Type u<VAR>V : Type v<VAR>DivisionRing K<VAR>AddCommGroup V<VAR>Module K V<VAR>FiniteDimensional K V<VAR>f g : V →ₗ[K] V<VAR>hfg : f * g = 1<GOAL>g * f = 1
<VAR>K : Type u<VAR>V : Type v<VAR>DivisionRing K<VAR>AddCommGroup V<VAR>Module K V<VAR>FiniteDimensional K V<VAR>f g : V →ₗ[K] V<GOAL>f * g = 1 ↔ g * f = 1
<VAR>K : Type u<VAR>V : Type v<VAR>DivisionRing K<VAR>AddCommGroup V<VAR>Module K V<VAR>FiniteDimensional K V<VAR>f g : V →ₗ[K] V<GOAL>f ∘ₗ g = LinearMap.id ↔ g ∘ₗ f = LinearMap.id
<VAR>K : Type u<VAR>V : Type v<VAR>DivisionRing K<VAR>AddCommGroup V<VAR>Module K V<VAR>p : Submodule K V<VAR>FiniteDimensional K ↥p<VAR>f : V →ₗ[K] V<VAR>h : ∀ x ∈ p, f x ∈ p<VAR>h' : Disjoint p (LinearMap.ker f)<GOAL>Submodule.comap f p = p ⊔ LinearMap.ker f
<VAR>K : Type u<VAR>V : Type v<VAR>DivisionRing K<VAR>AddCommGroup V<VAR>Module K V<VAR>FiniteDimensional K V<VAR>f g : V →ₗ[K] V<VAR>h : Commute f g<VAR>h' : Disjoint (LinearMap.ker f) (LinearMap.ker g)<GOAL>LinearMap.ker (f ∘ₗ g) = LinearMap.ker f ⊔ LinearMap.ker g
<VAR>K : Type u<VAR>V : Type v<VAR>DivisionRing K<VAR>AddCommGroup V<VAR>Module K V<VAR>FiniteDimensional K V<VAR>ι : Type u_1<VAR>f : ι → V →ₗ[K] V<VAR>s : Finset ι<VAR>comm : (↑s).Pairwise fun a b => Commute (f a) (f b)<VAR>h : s.SupIndep fun i => LinearMap.ker (f i)<GOAL>LinearMap.ker (s.noncommProd f comm) = ⨆ i ∈ s, LinearMap.ker (f i)
<VAR>K : Type u<VAR>V : Type v<VAR>DivisionRing K<VAR>AddCommGroup V<VAR>Module K V<VAR>FiniteDimensional K V<VAR>f : V →ₗ[K] V<VAR>h_inj : Function.Injective ⇑f<GOAL>⇑(LinearEquiv.ofInjectiveEndo f h_inj) = ⇑f
<VAR>K : Type u<VAR>V : Type v<VAR>DivisionRing K<VAR>AddCommGroup V<VAR>Module K V<VAR>FiniteDimensional K V<VAR>f : V →ₗ[K] V<VAR>h_inj : Function.Injective ⇑f<GOAL>f * ↑(LinearEquiv.ofInjectiveEndo f h_inj).symm = 1
<VAR>K : Type u<VAR>V : Type v<VAR>DivisionRing K<VAR>AddCommGroup V<VAR>Module K V<VAR>FiniteDimensional K V<VAR>f : V →ₗ[K] V<VAR>h_inj : Function.Injective ⇑f<GOAL>↑(LinearEquiv.ofInjectiveEndo f h_inj).symm * f = 1
<VAR>K : Type u<VAR>V : Type v<VAR>DivisionRing K<VAR>AddCommGroup V<VAR>Module K V<VAR>FiniteDimensional K V<VAR>f : V →ₗ[K] V<GOAL>IsUnit f ↔ LinearMap.ker f = ⊥
<VAR>K : Type u<VAR>V : Type v<VAR>DivisionRing K<VAR>AddCommGroup V<VAR>Module K V<VAR>FiniteDimensional K V<VAR>f : V →ₗ[K] V<GOAL>IsUnit f ↔ LinearMap.range f = ⊤
<VAR>K : Type u<VAR>V : Type v<VAR>DivisionRing K<VAR>AddCommGroup V<VAR>Module K V<VAR>FiniteDimensional K V<GOAL>FiniteDimensional.finrank K V = 0 ↔ ∀ (x : V), x = 0
<VAR>F : Type u_1<VAR>K : Type u_2<VAR>Field F<VAR>Ring K<VAR>IsDomain K<VAR>Algebra F K<VAR>FiniteDimensional F K<VAR>x : K<VAR>H : x ≠ 0<GOAL>∃ y, x * y = 1
<VAR>K : Type u<VAR>V : Type v<VAR>DivisionRing K<VAR>AddCommGroup V<VAR>Module K V<VAR>FiniteDimensional K V<GOAL>Monotone fun s => FiniteDimensional.finrank K ↥s
<VAR>K : Type u<VAR>V : Type v<VAR>DivisionRing K<VAR>AddCommGroup V<VAR>Module K V<VAR>v : V<VAR>hv : v ≠ 0<GOAL>FiniteDimensional.finrank K ↥(Submodule.span K {v}) = 1
<VAR>K : Type u<VAR>V : Type v<VAR>DivisionRing K<VAR>AddCommGroup V<VAR>Module K V<VAR>h : FiniteDimensional.finrank K V = 1<VAR>x : V<VAR>hx : x ≠ 0<VAR>y : V<GOAL>∃ c, c • x = y
<VAR>K : Type u<VAR>V : Type v<VAR>DivisionRing K<VAR>AddCommGroup V<VAR>Module K V<VAR>FiniteDimensional K V<VAR>s t : Set V<VAR>h : s ⊆ t<GOAL>Set.finrank K s ≤ Set.finrank K t
<VAR>K : Type u<VAR>V : Type v<VAR>DivisionRing K<VAR>AddCommGroup V<VAR>Module K V<VAR>v : V<VAR>nz : v ≠ 0<GOAL>FiniteDimensional.finrank K V = 1 ↔ Submodule.span K {v} = ⊤
<VAR>K : Type u<VAR>V : Type v<VAR>DivisionRing K<VAR>AddCommGroup V<VAR>Module K V<VAR>v : V<VAR>nz : v ≠ 0<GOAL>FiniteDimensional.finrank K V = 1 ↔ ∀ (w : V), ∃ c, c • v = w
<VAR>K : Type u<VAR>V : Type v<VAR>DivisionRing K<VAR>AddCommGroup V<VAR>Module K V<VAR>W : Type u_1<VAR>A : Type u_2<VAR>Semiring A<VAR>Module A V<VAR>AddCommGroup W<VAR>Module K W<VAR>Module A W<VAR>LinearMap.CompatibleSMul V W K A<VAR>h : FiniteDimensional.finrank K W = 1<VAR>f : V →ₗ[A] W<VAR>w : f ≠ 0<GOAL>Function.Surjective ⇑f
<VAR>F : Type u_1<VAR>E : Type u_2<VAR>Field F<VAR>Ring E<VAR>Algebra F E<VAR>S : Subalgebra F E<GOAL>FiniteDimensional F ↥(Subalgebra.toSubmodule S) ↔ FiniteDimensional F ↥S
<VAR>F : Type u_1<VAR>E : Type u_2<VAR>Field F<VAR>Ring E<VAR>Algebra F E<GOAL>FiniteDimensional F ↥⊥
<VAR>K : Type u<VAR>V : Type v<VAR>DivisionRing K<VAR>AddCommGroup V<VAR>Module K V<VAR>f : Module.End K V<VAR>k : ℕ<VAR>h : LinearMap.ker (f ^ k) = LinearMap.ker (f ^ k.succ)<VAR>m : ℕ<GOAL>LinearMap.ker (f ^ k) = LinearMap.ker (f ^ (k + m))
<VAR>k : Type u<VAR>Field k<VAR>self : IsSepClosed k<VAR>p : k[X]<GOAL>p.Separable → Polynomial.Splits (RingHom.id k) p
<VAR>k : Type u<VAR>Field k<VAR>K : Type v<VAR>Field K<VAR>IsSepClosed K<VAR>f : k →+* K<VAR>p : k[X]<VAR>h : p.Separable<GOAL>Polynomial.Splits f p
<VAR>k : Type u<VAR>Field k<VAR>K : Type v<VAR>Field K<VAR>IsSepClosed k<VAR>f : k →+* K<VAR>p : k[X]<VAR>h : p.Separable<GOAL>Polynomial.Splits f p
<VAR>k : Type u<VAR>Field k<VAR>IsSepClosed k<VAR>p : k[X]<VAR>hp : p.degree ≠ 0<VAR>hsep : p.Separable<GOAL>∃ x, p.IsRoot x
<VAR>k : Type u<VAR>Field k<VAR>IsSepClosed k<VAR>x : k<VAR>n : ℕ<VAR>hn : NeZero ↑n<GOAL>∃ z, z ^ n = x
<VAR>k : Type u<VAR>Field k<VAR>IsSepClosed k<VAR>x : k<VAR>h2 : NeZero 2<GOAL>∃ z, x = z * z
<VAR>k : Type u<VAR>Field k<VAR>IsSepClosed k<VAR>p : k[X]<VAR>hsep : p.Separable<GOAL>p.roots = 0 ↔ p = Polynomial.C (p.coeff 0)
<VAR>k : Type u<VAR>Field k<VAR>K : Type v<VAR>Field K<VAR>IsSepClosed K<VAR>f : k →+* K<VAR>p : k[X]<VAR>hp : p.degree ≠ 0<VAR>hsep : p.Separable<GOAL>∃ x, Polynomial.eval₂ f x p = 0
<VAR>k : Type u<VAR>Field k<VAR>K : Type v<VAR>Field K<VAR>IsSepClosed K<VAR>Algebra k K<VAR>p : k[X]<VAR>hp : p.degree ≠ 0<VAR>hsep : p.Separable<GOAL>∃ x, (Polynomial.aeval x) p = 0
<VAR>k : Type u<VAR>Field k<VAR>H : ∀ (p : k[X]), p.Monic → Irreducible p → p.Separable → ∃ x, Polynomial.eval x p = 0<GOAL>IsSepClosed k
<VAR>k : Type u<VAR>Field k<VAR>IsSepClosed k<VAR>p : k[X]<VAR>hp : Irreducible p<VAR>hsep : p.Separable<GOAL>p.degree = 1