ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>Ring S<VAR>Algebra R S<VAR>M N : Submodule R S<VAR>H : M.LinearDisjoint N<VAR>Module.Flat R ↥M<VAR>hc : ∀ (m n : ↥(M ⊓ N)), Commute ↑m ↑n<GOAL>Module.rank R ↥(M ⊓ N) ≤ 1
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>Ring S<VAR>Algebra R S<VAR>M N : Submodule R S<VAR>H : M.LinearDisjoint N<VAR>Module.Flat R ↥N<VAR>hc : ∀ (m n : ↥(M ⊓ N)), Commute ↑m ↑n<GOAL>Module.rank R ↥(M ⊓ N) ≤ 1
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>Ring S<VAR>Algebra R S<VAR>M : Submodule R S<VAR>H : M.LinearDisjoint M<VAR>Module.Flat R ↥M<VAR>hc : ∀ (m n : ↥M), Commute ↑m ↑n<GOAL>Module.rank R ↥M ≤ 1
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>M N : Submodule R S<VAR>H : M.LinearDisjoint N<VAR>Nontrivial R<VAR>Module.Flat R ↥M<VAR>a b : ↥(M ⊓ N)<GOAL>¬LinearIndependent R ![a, b]
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>M N : Submodule R S<VAR>H : M.LinearDisjoint N<VAR>Nontrivial R<VAR>Module.Flat R ↥N<VAR>a b : ↥(M ⊓ N)<GOAL>¬LinearIndependent R ![a, b]
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>M N : Submodule R S<VAR>H : M.LinearDisjoint N<VAR>Nontrivial R<VAR>hf : Module.Flat R ↥M ∨ Module.Flat R ↥N<VAR>a b : ↥(M ⊓ N)<GOAL>¬LinearIndependent R ![a, b]
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>M N : Submodule R S<VAR>H : M.LinearDisjoint N<VAR>hf : Module.Flat R ↥M ∨ Module.Flat R ↥N<GOAL>Module.rank R ↥(M ⊓ N) ≤ 1
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>M N : Submodule R S<VAR>H : M.LinearDisjoint N<VAR>Module.Flat R ↥M<GOAL>Module.rank R ↥(M ⊓ N) ≤ 1
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>M N : Submodule R S<VAR>H : M.LinearDisjoint N<VAR>Module.Flat R ↥N<GOAL>Module.rank R ↥(M ⊓ N) ≤ 1
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>M : Submodule R S<VAR>H : M.LinearDisjoint M<VAR>Module.Flat R ↥M<GOAL>Module.rank R ↥M ≤ 1
<VAR>R : Type u<VAR>M : Type v<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>ι : Type u_1<VAR>b : Basis ι R M<VAR>N : Submodule R M<VAR>ϕ : M →ₗ[R] R<VAR>hϕ : ∀ (ψ : M →ₗ[R] R), ¬Submodule.map ϕ N < Submodule.map ψ N<VAR>(Submodule.map ϕ N).IsPrincipal<VAR>hgen : Submodule.IsPrincipal.generator (Submodule.map ϕ N) = 0<GOAL>N = ⊥
<VAR>R : Type u<VAR>M : Type v<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>ι : Type u_1<VAR>N O : Submodule R M<VAR>b : Basis ι R ↥O<VAR>hNO : N ≤ O<VAR>ϕ : ↥O →ₗ[R] R<VAR>hϕ : ∀ (ψ : ↥O →ₗ[R] R), ¬ϕ.submoduleImage N < ψ.submoduleImage N<VAR>(ϕ.submoduleImage N).IsPrincipal<VAR>hgen : Submodule.IsPrincipal.generator (ϕ.submoduleImage N) = 0<GOAL>N = ⊥
<VAR>R : Type u_2<VAR>CommRing R<VAR>IsDomain R<VAR>I : Ideal R<VAR>Submodule.IsPrincipal I<VAR>x : R<VAR>hx : x ∈ I<GOAL>x ∣ Submodule.IsPrincipal.generator I ↔ I = Ideal.span {x}
<VAR>R : Type u_2<VAR>CommRing R<VAR>IsDomain R<VAR>IsPrincipalIdealRing R<VAR>M : Type u_3<VAR>AddCommGroup M<VAR>Module R M<VAR>N O : Submodule R M<VAR>hNO : N ≤ O<VAR>ϕ : ↥O →ₗ[R] R<VAR>hϕ : ∀ (ψ : ↥O →ₗ[R] R), ¬ϕ.submoduleImage N < ψ.submoduleImage N<VAR>(ϕ.submoduleImage N).IsPrincipal<VAR>y : M<VAR>yN : y ∈ N<VAR>ϕy_eq : ϕ ⟨y, ⋯⟩ = Submodule.IsPrincipal.generator (ϕ.submoduleImage N)<VAR>ψ : ↥O →ₗ[R] R<GOAL>Submodule.IsPrincipal.generator (ϕ.submoduleImage N) ∣ ψ ⟨y, ⋯⟩
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>CommRing R<VAR>IsDomain R<VAR>IsPrincipalIdealRing R<VAR>Finite ι<VAR>O : Type u_4<VAR>AddCommGroup O<VAR>Module R O<VAR>M N : Submodule R O<VAR>b'M : Basis ι R ↥M<VAR>N_bot : N ≠ ⊥<VAR>N_le_M : N ≤ M<GOAL>∃ y ∈ M, ∃ a, a • y ∈ N ∧ ∃ M' ≤ M, ∃ N' ≤ N, N' ≤ M' ∧ (∀ (c : R), ∀ z ∈ M', c • y + z = 0 → c = 0) ∧ (∀ (c : R), ∀ z ∈ N', c • a • y + z = 0 → c = 0) ∧ ∀ (n' : ℕ) (bN' : Basis (Fin n') R ↥N'), ∃ bN, ∀ (m' : ℕ) (hn'm' : n' ≤ m') (bM' : Basis (Fin m') R ↥M'), ∃ (hnm : n' + 1 ≤ m' + 1), ∃ bM, ∀ (as : Fin n' → R), (∀ (i : Fin n'), ↑(bN' i) = as i • ↑(bM' (Fin.castLE hn'm' i))) → ∃ as', ∀ (i : Fin (n' + 1)), ↑(bN i) = as' i • ↑(bM (Fin.castLE hnm i))
<VAR>R : Type u_2<VAR>CommRing R<VAR>IsDomain R<VAR>IsPrincipalIdealRing R<VAR>M : Type u_3<VAR>AddCommGroup M<VAR>Module R M<VAR>ι : Type u_4<VAR>Finite ι<VAR>b : Basis ι R M<VAR>N : Submodule R M<GOAL>∃ n, Nonempty (Basis (Fin n) R ↥N)
<VAR>R : Type u_2<VAR>CommRing R<VAR>IsDomain R<VAR>IsPrincipalIdealRing R<VAR>M : Type u_3<VAR>AddCommGroup M<VAR>Module R M<VAR>ι : Type u_4<VAR>Finite ι<VAR>b : Basis ι R M<GOAL>Submodule.basisOfPid b ⊥ = ⟨0, Basis.empty ↥⊥⟩
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>CommRing R<VAR>IsDomain R<VAR>IsPrincipalIdealRing R<VAR>M : Type u_3<VAR>AddCommGroup M<VAR>Module R M<VAR>Finite ι<VAR>s : ι → M<VAR>hs : Submodule.span R (Set.range s) = ⊤<VAR>NoZeroSMulDivisors R M<GOAL>Module.Free R M
<VAR>R : Type u_2<VAR>CommRing R<VAR>IsDomain R<VAR>IsPrincipalIdealRing R<VAR>M : Type u_3<VAR>AddCommGroup M<VAR>Module R M<VAR>Module.Finite R M<GOAL>Module.Free R M ↔ NoZeroSMulDivisors R M
<VAR>R : Type u_2<VAR>CommRing R<VAR>M : Type u_3<VAR>AddCommGroup M<VAR>Module R M<VAR>N : Submodule R M<VAR>ι : Type u_4<VAR>n : ℕ<VAR>self : Basis.SmithNormalForm N ι n<VAR>i : Fin n<GOAL>↑(self.bN i) = self.a i • self.bM (self.f i)
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>CommRing R<VAR>M : Type u_3<VAR>AddCommGroup M<VAR>Module R M<VAR>n : ℕ<VAR>N : Submodule R M<VAR>snf : Basis.SmithNormalForm N ι n<VAR>m : ↥N<VAR>i : ι<VAR>hi : i ∉ Set.range ⇑snf.f<GOAL>(snf.bM.repr ↑m) i = 0
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>CommRing R<VAR>M : Type u_3<VAR>AddCommGroup M<VAR>Module R M<VAR>n : ℕ<VAR>N : Submodule R M<VAR>snf : Basis.SmithNormalForm N ι n<VAR>i : ι<VAR>hi : i ∉ Set.range ⇑snf.f<GOAL>N ≤ LinearMap.ker (snf.bM.coord i)
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>CommRing R<VAR>M : Type u_3<VAR>AddCommGroup M<VAR>Module R M<VAR>n : ℕ<VAR>N : Submodule R M<VAR>snf : Basis.SmithNormalForm N ι n<VAR>m : ↥N<VAR>i : Fin n<GOAL>(snf.bM.repr ↑m) (snf.f i) = (snf.bN.repr (snf.a i • m)) i
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>CommRing R<VAR>M : Type u_3<VAR>AddCommGroup M<VAR>Module R M<VAR>n : ℕ<VAR>N : Submodule R M<VAR>snf : Basis.SmithNormalForm N ι n<VAR>m : ↥N<GOAL>⇑(snf.bM.repr ↑m) ∘ ⇑snf.f = snf.a • ⇑(snf.bN.repr m)
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>CommRing R<VAR>M : Type u_3<VAR>AddCommGroup M<VAR>Module R M<VAR>n : ℕ<VAR>N : Submodule R M<VAR>snf : Basis.SmithNormalForm N ι n<VAR>i : Fin n<GOAL>snf.bM.coord (snf.f i) ∘ₗ N.subtype = snf.a i • snf.bN.coord i
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>CommRing R<VAR>M : Type u_3<VAR>AddCommGroup M<VAR>Module R M<VAR>n : ℕ<VAR>N : Submodule R M<VAR>snf : Basis.SmithNormalForm N ι n<VAR>Fintype ι<VAR>DecidableEq ι<VAR>f : M →ₗ[R] M<VAR>hf : ∀ (x : M), f x ∈ N<VAR>hf' : ∀ x ∈ N, f x ∈ N := ⋯<VAR>i : Fin n<GOAL>(LinearMap.toMatrix snf.bN snf.bN) (f.restrict hf') i i = (LinearMap.toMatrix snf.bM snf.bM) f (snf.f i) (snf.f i)
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>CommRing R<VAR>IsDomain R<VAR>IsPrincipalIdealRing R<VAR>M : Type u_3<VAR>AddCommGroup M<VAR>Module R M<VAR>Finite ι<VAR>b : Basis ι R M<VAR>N O : Submodule R M<VAR>N_le_O : N ≤ O<GOAL>∃ n o, ∃ (hno : n ≤ o), ∃ bO bN a, ∀ (i : Fin n), ↑(bN i) = a i • ↑(bO (Fin.castLE hno i))
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>CommRing R<VAR>IsDomain R<VAR>IsPrincipalIdealRing R<VAR>S : Type u_4<VAR>CommRing S<VAR>IsDomain S<VAR>Algebra R S<VAR>Finite ι<VAR>b : Basis ι R S<VAR>I : Ideal S<VAR>hI : I ≠ ⊥<GOAL>∃ b' a ab', ∀ (i : ι), ↑(ab' i) = a i • b' i
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>CommRing R<VAR>IsDomain R<VAR>IsPrincipalIdealRing R<VAR>S : Type u_4<VAR>CommRing S<VAR>IsDomain S<VAR>Algebra R S<VAR>Finite ι<VAR>b : Basis ι R S<VAR>I : Ideal S<VAR>hI : I ≠ ⊥<VAR>i : ι<GOAL>↑((Ideal.selfBasis b I hI) i) = Ideal.smithCoeffs b I hI i • (Ideal.ringBasis b I hI) i
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>CommRing R<VAR>IsDomain R<VAR>IsPrincipalIdealRing R<VAR>S : Type u_4<VAR>CommRing S<VAR>IsDomain S<VAR>Algebra R S<VAR>Finite ι<VAR>b : Basis ι R S<VAR>I : Ideal S<VAR>hI : I ≠ ⊥<VAR>i : ι<GOAL>Ideal.smithCoeffs b I hI i ≠ 0
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>M : Type u_3<VAR>ι : Type u_4<VAR>CommSemiring R<VAR>Semiring S<VAR>AddCommMonoid M<VAR>Algebra R S<VAR>Module R M<VAR>Module S M<VAR>IsScalarTower R S M<VAR>hinj : Function.Injective ⇑(algebraMap R S)<VAR>v : ι → M<VAR>li : LinearIndependent S v<GOAL>LinearIndependent R v
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>B : LinearMap.BilinForm R M<VAR>x y : M<GOAL>B.IsOrtho x y ↔ (B x) y = 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>B : LinearMap.BilinForm R M<VAR>x : M<GOAL>B.IsOrtho 0 x
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>B : LinearMap.BilinForm R M<VAR>x : M<GOAL>B.IsOrtho x 0
<VAR>V : Type u_5<VAR>K : Type u_6<VAR>Field K<VAR>AddCommGroup V<VAR>Module K V<VAR>B : LinearMap.BilinForm K V<VAR>x : V<VAR>hx₁ : ¬B.IsOrtho x x<GOAL>x ≠ 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>B : LinearMap.BilinForm R M<VAR>H : B.IsRefl<VAR>x y : M<GOAL>B.IsOrtho x y ↔ B.IsOrtho y x
<VAR>R₁ : Type u_3<VAR>M₁ : Type u_4<VAR>CommRing R₁<VAR>AddCommGroup M₁<VAR>Module R₁ M₁<VAR>B₁ : LinearMap.BilinForm R₁ M₁<VAR>H : B₁.IsAlt<VAR>x y : M₁<GOAL>B₁.IsOrtho x y ↔ B₁.IsOrtho y x
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>B : LinearMap.BilinForm R M<VAR>H : B.IsSymm<VAR>x y : M<GOAL>B.IsOrtho x y ↔ B.IsOrtho y x
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>n : Type w<VAR>B : LinearMap.BilinForm R M<VAR>v : n → M<GOAL>B.iIsOrtho v ↔ ∀ (i j : n), i ≠ j → (B (v i)) (v j) = 0
<VAR>R₄ : Type u_7<VAR>M₄ : Type u_8<VAR>CommRing R₄<VAR>IsDomain R₄<VAR>AddCommGroup M₄<VAR>Module R₄ M₄<VAR>G : LinearMap.BilinForm R₄ M₄<VAR>x y : M₄<VAR>a : R₄<VAR>ha : a ≠ 0<GOAL>G.IsOrtho (a • x) y ↔ G.IsOrtho x y
<VAR>R₄ : Type u_7<VAR>M₄ : Type u_8<VAR>CommRing R₄<VAR>IsDomain R₄<VAR>AddCommGroup M₄<VAR>Module R₄ M₄<VAR>G : LinearMap.BilinForm R₄ M₄<VAR>x y : M₄<VAR>a : R₄<VAR>ha : a ≠ 0<GOAL>G.IsOrtho x (a • y) ↔ G.IsOrtho x y
<VAR>V : Type u_5<VAR>K : Type u_6<VAR>Field K<VAR>AddCommGroup V<VAR>Module K V<VAR>n : Type w<VAR>B : LinearMap.BilinForm K V<VAR>v : n → V<VAR>hv₁ : B.iIsOrtho v<VAR>hv₂ : ∀ (i : n), ¬B.IsOrtho (v i) (v i)<GOAL>LinearIndependent K v
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>B : LinearMap.BilinForm R M<VAR>N : Submodule R M<VAR>m : M<GOAL>m ∈ B.orthogonal N ↔ ∀ n ∈ N, B.IsOrtho n m
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>B : LinearMap.BilinForm R M<GOAL>B.orthogonal ⊥ = ⊤
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>B : LinearMap.BilinForm R M<VAR>N L : Submodule R M<VAR>h : N ≤ L<GOAL>B.orthogonal L ≤ B.orthogonal N
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>B : LinearMap.BilinForm R M<VAR>N : Submodule R M<VAR>b : B.IsRefl<GOAL>N ≤ B.orthogonal (B.orthogonal N)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>B : LinearMap.BilinForm R M<VAR>hB : B.Nondegenerate<VAR>hB₀ : B.IsRefl<GOAL>B.orthogonal ⊤ = ⊥
<VAR>V : Type u_5<VAR>K : Type u_6<VAR>Field K<VAR>AddCommGroup V<VAR>Module K V<VAR>B : LinearMap.BilinForm K V<VAR>x : V<VAR>hx : ¬B.IsOrtho x x<GOAL>Submodule.span K {x} ⊓ B.orthogonal (Submodule.span K {x}) = ⊥
<VAR>V : Type u_5<VAR>K : Type u_6<VAR>Field K<VAR>AddCommGroup V<VAR>Module K V<VAR>B : LinearMap.BilinForm K V<VAR>x : V<GOAL>B.orthogonal (Submodule.span K {x}) = LinearMap.ker (B.toLinHomAux₁ x)
<VAR>V : Type u_5<VAR>K : Type u_6<VAR>Field K<VAR>AddCommGroup V<VAR>Module K V<VAR>B : LinearMap.BilinForm K V<VAR>x : V<VAR>hx : ¬B.IsOrtho x x<GOAL>Submodule.span K {x} ⊔ B.orthogonal (Submodule.span K {x}) = ⊤
<VAR>V : Type u_5<VAR>K : Type u_6<VAR>Field K<VAR>AddCommGroup V<VAR>Module K V<VAR>B : LinearMap.BilinForm K V<VAR>x : V<VAR>hx : ¬B.IsOrtho x x<GOAL>IsCompl (Submodule.span K {x}) (B.orthogonal (Submodule.span K {x}))
<VAR>R₁ : Type u_3<VAR>M₁ : Type u_4<VAR>CommRing R₁<VAR>AddCommGroup M₁<VAR>Module R₁ M₁<VAR>B : LinearMap.BilinForm R₁ M₁<VAR>b : B.IsRefl<VAR>W : Submodule R₁ M₁<VAR>hW : Disjoint W (B.orthogonal W)<GOAL>(B.restrict W).Nondegenerate
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>n : Type w<VAR>Nontrivial R<VAR>B : LinearMap.BilinForm R M<VAR>v : Basis n R M<VAR>h : B.iIsOrtho ⇑v<VAR>hB : B.Nondegenerate<VAR>i : n<GOAL>¬B.IsOrtho (v i) (v i)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>n : Type w<VAR>Nontrivial R<VAR>NoZeroDivisors R<VAR>B : LinearMap.BilinForm R M<VAR>v : Basis n R M<VAR>hO : B.iIsOrtho ⇑v<GOAL>B.Nondegenerate ↔ ∀ (i : n), ¬B.IsOrtho (v i) (v i)
<VAR>V : Type u_5<VAR>K : Type u_6<VAR>Field K<VAR>AddCommGroup V<VAR>Module K V<VAR>B : LinearMap.BilinForm K V<VAR>W : Subspace K V<VAR>b : B.IsRefl<GOAL>Submodule.map (Submodule.subtype W) (LinearMap.ker (LinearMap.domRestrict B W)) = W ⊓ B.orthogonal ⊤
<VAR>V : Type u_5<VAR>K : Type u_6<VAR>Field K<VAR>AddCommGroup V<VAR>Module K V<VAR>B : LinearMap.BilinForm K V<VAR>W : Subspace K V<GOAL>(LinearMap.range (LinearMap.domRestrict B W)).dualCoannihilator = B.orthogonal W
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>p q : Submodule R M<VAR>hpq : Codisjoint p q<VAR>B : LinearMap.BilinForm R M<VAR>hB : ∀ x ∈ p, ∀ y ∈ q, (B x) y = 0<GOAL>LinearMap.ker (B.restrict p) = Submodule.comap p.subtype (LinearMap.ker B)
<VAR>V : Type u_5<VAR>K : Type u_6<VAR>Field K<VAR>AddCommGroup V<VAR>Module K V<VAR>FiniteDimensional K V<VAR>B : LinearMap.BilinForm K V<VAR>b₁ : B.IsRefl<VAR>W : Submodule K V<GOAL>FiniteDimensional.finrank K ↥W + FiniteDimensional.finrank K ↥(B.orthogonal W) = FiniteDimensional.finrank K V + FiniteDimensional.finrank K ↥(W ⊓ B.orthogonal ⊤)
<VAR>V : Type u_5<VAR>K : Type u_6<VAR>Field K<VAR>AddCommGroup V<VAR>Module K V<VAR>FiniteDimensional K V<VAR>B : LinearMap.BilinForm K V<VAR>hB : B.Nondegenerate<VAR>hB₀ : B.IsRefl<VAR>W : Submodule K V<GOAL>FiniteDimensional.finrank K ↥(B.orthogonal W) = FiniteDimensional.finrank K V - FiniteDimensional.finrank K ↥W
<VAR>V : Type u_5<VAR>K : Type u_6<VAR>Field K<VAR>AddCommGroup V<VAR>Module K V<VAR>FiniteDimensional K V<VAR>B : LinearMap.BilinForm K V<VAR>hB : B.Nondegenerate<VAR>hB₀ : B.IsRefl<VAR>W : Submodule K V<GOAL>B.orthogonal (B.orthogonal W) = W
<VAR>V : Type u_5<VAR>K : Type u_6<VAR>Field K<VAR>AddCommGroup V<VAR>Module K V<VAR>FiniteDimensional K V<VAR>B : LinearMap.BilinForm K V<VAR>W : Submodule K V<VAR>hB₀ : B.IsRefl<GOAL>IsCompl W (B.orthogonal W) ↔ Disjoint W (B.orthogonal W)
<VAR>V : Type u_5<VAR>K : Type u_6<VAR>Field K<VAR>AddCommGroup V<VAR>Module K V<VAR>FiniteDimensional K V<VAR>B : LinearMap.BilinForm K V<VAR>W : Submodule K V<VAR>b₁ : B.IsRefl<VAR>b₂ : (B.restrict W).Nondegenerate<GOAL>IsCompl W (B.orthogonal W)
<VAR>V : Type u_5<VAR>K : Type u_6<VAR>Field K<VAR>AddCommGroup V<VAR>Module K V<VAR>FiniteDimensional K V<VAR>B : LinearMap.BilinForm K V<VAR>W : Submodule K V<VAR>b₁ : B.IsRefl<GOAL>(B.restrict W).Nondegenerate ↔ IsCompl W (B.orthogonal W)
<VAR>V : Type u_5<VAR>K : Type u_6<VAR>Field K<VAR>AddCommGroup V<VAR>Module K V<VAR>FiniteDimensional K V<VAR>B : LinearMap.BilinForm K V<VAR>W : Submodule K V<VAR>b₁ : B.IsRefl<VAR>b₂ : (B.restrict W).Nondegenerate<GOAL>B.orthogonal W = ⊤ ↔ W = ⊥
<VAR>V : Type u_5<VAR>K : Type u_6<VAR>Field K<VAR>AddCommGroup V<VAR>Module K V<VAR>FiniteDimensional K V<VAR>B : LinearMap.BilinForm K V<VAR>W : Submodule K V<VAR>b₁ : B.IsRefl<VAR>b₂ : (B.restrict W).Nondegenerate<VAR>b₃ : B.orthogonal W = ⊥<GOAL>W = ⊤
<VAR>V : Type u_5<VAR>K : Type u_6<VAR>Field K<VAR>AddCommGroup V<VAR>Module K V<VAR>FiniteDimensional K V<VAR>B : LinearMap.BilinForm K V<VAR>W : Submodule K V<VAR>b₁ : B.IsRefl<VAR>b₂ : (B.restrict W).Nondegenerate<VAR>b₃ : B.Nondegenerate<GOAL>B.orthogonal W = ⊥ ↔ W = ⊤
<VAR>V : Type u_5<VAR>K : Type u_6<VAR>Field K<VAR>AddCommGroup V<VAR>Module K V<VAR>B : LinearMap.BilinForm K V<VAR>W : Submodule K V<VAR>b₁ : B.IsRefl<GOAL>W ⊓ B.orthogonal W ≤ Submodule.map W.subtype (LinearMap.ker (B.restrict W))
<VAR>V : Type u_5<VAR>K : Type u_6<VAR>Field K<VAR>AddCommGroup V<VAR>Module K V<VAR>B : LinearMap.BilinForm K V<VAR>b₁ : B.Nondegenerate<VAR>b₂ : B.IsRefl<VAR>x : V<VAR>hx : ¬B.IsOrtho x x<GOAL>(B.restrict (B.orthogonal (Submodule.span K {x}))).Nondegenerate
<VAR>R : Type u_1<VAR>StrictOrderedCommSemiring R<VAR>M : Type u_2<VAR>AddCommMonoid M<VAR>Module R M<VAR>y : M<GOAL>SameRay R 0 y
<VAR>R : Type u_1<VAR>StrictOrderedCommSemiring R<VAR>M : Type u_2<VAR>AddCommMonoid M<VAR>Module R M<VAR>x : M<GOAL>SameRay R x 0
<VAR>R : Type u_1<VAR>StrictOrderedCommSemiring R<VAR>M : Type u_2<VAR>AddCommMonoid M<VAR>Module R M<VAR>Subsingleton M<VAR>x y : M<GOAL>SameRay R x y
<VAR>R : Type u_1<VAR>StrictOrderedCommSemiring R<VAR>M : Type u_2<VAR>AddCommMonoid M<VAR>Module R M<VAR>Subsingleton R<VAR>x y : M<GOAL>SameRay R x y
<VAR>R : Type u_1<VAR>StrictOrderedCommSemiring R<VAR>M : Type u_2<VAR>AddCommMonoid M<VAR>Module R M<VAR>x : M<GOAL>SameRay R x x
<VAR>R : Type u_1<VAR>StrictOrderedCommSemiring R<VAR>M : Type u_2<VAR>AddCommMonoid M<VAR>Module R M<VAR>x y : M<VAR>h : SameRay R x y<GOAL>SameRay R y x
<VAR>R : Type u_1<VAR>StrictOrderedCommSemiring R<VAR>M : Type u_2<VAR>AddCommMonoid M<VAR>Module R M<VAR>x y : M<VAR>h : SameRay R x y<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<GOAL>∃ r₁ r₂, 0 < r₁ ∧ 0 < r₂ ∧ r₁ • x = r₂ • y
<VAR>R : Type u_1<VAR>StrictOrderedCommSemiring R<VAR>M : Type u_2<VAR>AddCommMonoid M<VAR>Module R M<VAR>x y : M<GOAL>SameRay R x y ↔ SameRay R y x
<VAR>R : Type u_1<VAR>StrictOrderedCommSemiring R<VAR>M : Type u_2<VAR>AddCommMonoid M<VAR>Module R M<VAR>x y z : M<VAR>hxy : SameRay R x y<VAR>hyz : SameRay R y z<VAR>hy : y = 0 → x = 0 ∨ z = 0<GOAL>SameRay R x z
<VAR>R : Type u_1<VAR>StrictOrderedCommSemiring R<VAR>M : Type u_2<VAR>AddCommMonoid M<VAR>Module R M<VAR>S : Type u_5<VAR>OrderedCommSemiring S<VAR>Algebra S R<VAR>Module S M<VAR>SMulPosMono S R<VAR>IsScalarTower S R M<VAR>a : S<VAR>v : M<VAR>h : 0 ≤ a<GOAL>SameRay R v (a • v)
<VAR>R : Type u_1<VAR>StrictOrderedCommSemiring R<VAR>M : Type u_2<VAR>AddCommMonoid M<VAR>Module R M<VAR>S : Type u_5<VAR>OrderedCommSemiring S<VAR>Algebra S R<VAR>Module S M<VAR>SMulPosMono S R<VAR>IsScalarTower S R M<VAR>a : S<VAR>v : M<VAR>ha : 0 ≤ a<GOAL>SameRay R (a • v) v
<VAR>R : Type u_1<VAR>StrictOrderedCommSemiring R<VAR>M : Type u_2<VAR>AddCommMonoid M<VAR>Module R M<VAR>S : Type u_5<VAR>OrderedCommSemiring S<VAR>Algebra S R<VAR>Module S M<VAR>SMulPosMono S R<VAR>IsScalarTower S R M<VAR>a : S<VAR>v : M<VAR>ha : 0 < a<GOAL>SameRay R v (a • v)
<VAR>R : Type u_1<VAR>StrictOrderedCommSemiring R<VAR>M : Type u_2<VAR>AddCommMonoid M<VAR>Module R M<VAR>S : Type u_5<VAR>OrderedCommSemiring S<VAR>Algebra S R<VAR>Module S M<VAR>SMulPosMono S R<VAR>IsScalarTower S R M<VAR>a : S<VAR>v : M<VAR>ha : 0 < a<GOAL>SameRay R (a • v) v
<VAR>R : Type u_1<VAR>StrictOrderedCommSemiring R<VAR>M : Type u_2<VAR>AddCommMonoid M<VAR>Module R M<VAR>x y : M<VAR>S : Type u_5<VAR>OrderedCommSemiring S<VAR>Algebra S R<VAR>Module S M<VAR>SMulPosMono S R<VAR>IsScalarTower S R M<VAR>a : S<VAR>h : SameRay R x y<VAR>ha : 0 ≤ a<GOAL>SameRay R x (a • y)
<VAR>R : Type u_1<VAR>StrictOrderedCommSemiring R<VAR>M : Type u_2<VAR>AddCommMonoid M<VAR>Module R M<VAR>x y : M<VAR>S : Type u_5<VAR>OrderedCommSemiring S<VAR>Algebra S R<VAR>Module S M<VAR>SMulPosMono S R<VAR>IsScalarTower S R M<VAR>a : S<VAR>h : SameRay R x y<VAR>ha : 0 ≤ a<GOAL>SameRay R (a • x) y
<VAR>R : Type u_1<VAR>StrictOrderedCommSemiring R<VAR>M : Type u_2<VAR>AddCommMonoid M<VAR>Module R M<VAR>x y : M<VAR>S : Type u_5<VAR>OrderedCommSemiring S<VAR>Algebra S R<VAR>Module S M<VAR>SMulPosMono S R<VAR>IsScalarTower S R M<VAR>a : S<VAR>h : SameRay R x y<VAR>ha : 0 < a<GOAL>SameRay R x (a • y)
<VAR>R : Type u_1<VAR>StrictOrderedCommSemiring R<VAR>M : Type u_2<VAR>AddCommMonoid M<VAR>Module R M<VAR>x y : M<VAR>S : Type u_5<VAR>OrderedCommSemiring S<VAR>Algebra S R<VAR>Module S M<VAR>SMulPosMono S R<VAR>IsScalarTower S R M<VAR>a : S<VAR>h : SameRay R x y<VAR>hr : 0 < a<GOAL>SameRay R (a • x) y
<VAR>R : Type u_1<VAR>StrictOrderedCommSemiring R<VAR>M : Type u_2<VAR>AddCommMonoid M<VAR>Module R M<VAR>N : Type u_3<VAR>AddCommMonoid N<VAR>Module R N<VAR>x y : M<VAR>f : M →ₗ[R] N<VAR>h : SameRay R x y<GOAL>SameRay R (f x) (f y)
<VAR>R : Type u_1<VAR>StrictOrderedCommSemiring R<VAR>M : Type u_2<VAR>AddCommMonoid M<VAR>Module R M<VAR>N : Type u_3<VAR>AddCommMonoid N<VAR>Module R N<VAR>x y : M<VAR>F : Type u_6<VAR>FunLike F M N<VAR>LinearMapClass F R M N<VAR>f : F<VAR>hf : Function.Injective ⇑f<GOAL>SameRay R (f x) (f y) ↔ SameRay R x y
<VAR>R : Type u_1<VAR>StrictOrderedCommSemiring R<VAR>M : Type u_2<VAR>AddCommMonoid M<VAR>Module R M<VAR>N : Type u_3<VAR>AddCommMonoid N<VAR>Module R N<VAR>x y : M<VAR>e : M ≃ₗ[R] N<GOAL>SameRay R (e x) (e y) ↔ SameRay R x y
<VAR>R : Type u_1<VAR>StrictOrderedCommSemiring R<VAR>M : Type u_2<VAR>AddCommMonoid M<VAR>Module R M<VAR>x y : M<VAR>S : Type u_6<VAR>Monoid S<VAR>DistribMulAction S M<VAR>SMulCommClass R S M<VAR>h : SameRay R x y<VAR>s : S<GOAL>SameRay R (s • x) (s • y)
<VAR>R : Type u_1<VAR>StrictOrderedCommSemiring R<VAR>M : Type u_2<VAR>AddCommMonoid M<VAR>Module R M<VAR>x y z : M<VAR>hx : SameRay R x z<VAR>hy : SameRay R y z<GOAL>SameRay R (x + y) z
<VAR>R : Type u_1<VAR>StrictOrderedCommSemiring R<VAR>M : Type u_2<VAR>AddCommMonoid M<VAR>Module R M<VAR>x y z : M<VAR>hy : SameRay R x y<VAR>hz : SameRay R x z<GOAL>SameRay R x (y + z)
<VAR>R : Type u_1<VAR>StrictOrderedCommSemiring R<VAR>M : Type u_2<VAR>AddCommMonoid M<VAR>Module R M<VAR>v₁ v₂ : RayVector R M<GOAL>v₁ ≈ v₂ ↔ SameRay R ↑v₁ ↑v₂
<VAR>R : Type u_1<VAR>StrictOrderedCommSemiring R<VAR>M : Type u_2<VAR>AddCommMonoid M<VAR>Module R M<VAR>C : Module.Ray R M → Prop<VAR>h : ∀ (v : M) (hv : v ≠ 0), C (rayOfNeZero R v hv)<VAR>x : Module.Ray R M<GOAL>C x
<VAR>R : Type u_1<VAR>StrictOrderedCommSemiring R<VAR>M : Type u_2<VAR>AddCommMonoid M<VAR>Module R M<VAR>v₁ v₂ : M<VAR>hv₁ : v₁ ≠ 0<VAR>hv₂ : v₂ ≠ 0<GOAL>rayOfNeZero R v₁ hv₁ = rayOfNeZero R v₂ hv₂ ↔ SameRay R v₁ v₂
<VAR>R : Type u_1<VAR>StrictOrderedCommSemiring R<VAR>M : Type u_2<VAR>AddCommMonoid M<VAR>Module R M<VAR>v : M<VAR>h : v ≠ 0<VAR>r : R<VAR>hr : 0 < r<VAR>hrv : r • v ≠ 0<GOAL>rayOfNeZero R (r • v) hrv = rayOfNeZero R v h
<VAR>R : Type u_1<VAR>StrictOrderedCommSemiring R<VAR>M : Type u_2<VAR>AddCommMonoid M<VAR>Module R M<VAR>N : Type u_3<VAR>AddCommMonoid N<VAR>Module R N<VAR>e : M ≃ₗ[R] N<VAR>v : M<VAR>hv : v ≠ 0<GOAL>(Module.Ray.map e) (rayOfNeZero R v hv) = rayOfNeZero R (e v) ⋯
<VAR>R : Type u_1<VAR>StrictOrderedCommSemiring R<VAR>M : Type u_2<VAR>AddCommMonoid M<VAR>Module R M<GOAL>Module.Ray.map (LinearEquiv.refl R M) = Equiv.refl (Module.Ray R M)
<VAR>R : Type u_1<VAR>StrictOrderedCommSemiring R<VAR>M : Type u_2<VAR>AddCommMonoid M<VAR>Module R M<VAR>N : Type u_3<VAR>AddCommMonoid N<VAR>Module R N<VAR>e : M ≃ₗ[R] N<GOAL>(Module.Ray.map e).symm = Module.Ray.map e.symm
<VAR>R : Type u_1<VAR>StrictOrderedCommSemiring R<VAR>M : Type u_2<VAR>AddCommMonoid M<VAR>Module R M<VAR>e : M ≃ₗ[R] M<VAR>v : Module.Ray R M<GOAL>e • v = (Module.Ray.map e) v
<VAR>R : Type u_1<VAR>StrictOrderedCommSemiring R<VAR>M : Type u_2<VAR>AddCommMonoid M<VAR>Module R M<VAR>G : Type u_5<VAR>Group G<VAR>DistribMulAction G M<VAR>SMulCommClass R G M<VAR>g : G<VAR>v : M<VAR>hv : v ≠ 0<GOAL>g • rayOfNeZero R v hv = rayOfNeZero R (g • v) ⋯
<VAR>R : Type u_1<VAR>StrictOrderedCommSemiring R<VAR>M : Type u_2<VAR>AddCommMonoid M<VAR>Module R M<VAR>u : Rˣ<VAR>hu : 0 < ↑u<VAR>v : Module.Ray R M<GOAL>u • v = v
<VAR>R : Type u_1<VAR>StrictOrderedCommSemiring R<VAR>M : Type u_2<VAR>AddCommMonoid M<VAR>Module R M<VAR>x : Module.Ray R M<GOAL>⟦x.someRayVector⟧ = x
<VAR>R : Type u_1<VAR>StrictOrderedCommSemiring R<VAR>M : Type u_2<VAR>AddCommMonoid M<VAR>Module R M<VAR>x : Module.Ray R M<GOAL>x.someVector ≠ 0
<VAR>R : Type u_1<VAR>StrictOrderedCommSemiring R<VAR>M : Type u_2<VAR>AddCommMonoid M<VAR>Module R M<VAR>x : Module.Ray R M<GOAL>rayOfNeZero R x.someVector ⋯ = x