ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>Semiring 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>ι : Type u_7<VAR>ι' : Type u_8<VAR>S : Type u_12<VAR>Monoid S<VAR>DistribMulAction S N<VAR>SMulCommClass R S N<VAR>σ : ι ≃ ι'<VAR>c : S<VAR>f : M [⋀^ι]→ₗ[R] N<GOAL>AlternatingMap.domDomCongr σ (c • f) = c • AlternatingMap.domDomCongr σ f
<VAR>R : Type u_1<VAR>Semiring 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>ι : Type u_7<VAR>ι' : Type u_8<VAR>σ : ι ≃ ι'<VAR>f : M [⋀^ι]→ₗ[R] N<GOAL>(AlternatingMap.domDomCongrEquiv σ) f = AlternatingMap.domDomCongr σ f
<VAR>R : Type u_1<VAR>Semiring 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>ι : Type u_7<VAR>ι' : Type u_8<VAR>σ : ι ≃ ι'<VAR>f : M [⋀^ι']→ₗ[R] N<GOAL>(AlternatingMap.domDomCongrEquiv σ).symm f = AlternatingMap.domDomCongr σ.symm f
<VAR>R : Type u_1<VAR>Semiring 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>ι : Type u_7<VAR>ι' : Type u_8<VAR>S : Type u_12<VAR>Semiring S<VAR>Module S N<VAR>SMulCommClass R S N<VAR>σ : ι ≃ ι'<VAR>f : M [⋀^ι]→ₗ[R] N<GOAL>(AlternatingMap.domDomCongrₗ S σ) f = AlternatingMap.domDomCongr σ f
<VAR>R : Type u_1<VAR>Semiring 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>ι : Type u_7<VAR>ι' : Type u_8<VAR>S : Type u_12<VAR>Semiring S<VAR>Module S N<VAR>SMulCommClass R S N<VAR>σ : ι ≃ ι'<VAR>f : M [⋀^ι']→ₗ[R] N<GOAL>(AlternatingMap.domDomCongrₗ S σ).symm f = AlternatingMap.domDomCongr σ.symm f
<VAR>R : Type u_1<VAR>Semiring 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>ι : Type u_7<VAR>S : Type u_12<VAR>Semiring S<VAR>Module S N<VAR>SMulCommClass R S N<GOAL>AlternatingMap.domDomCongrₗ S (Equiv.refl ι) = LinearEquiv.refl S (M [⋀^ι]→ₗ[R] N)
<VAR>R : Type u_1<VAR>Semiring 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>ι : Type u_7<VAR>ι' : Type u_8<VAR>S : Type u_12<VAR>Semiring S<VAR>Module S N<VAR>SMulCommClass R S N<VAR>σ : ι ≃ ι'<GOAL>↑(AlternatingMap.domDomCongrₗ S σ) = AlternatingMap.domDomCongrEquiv σ
<VAR>R : Type u_1<VAR>Semiring 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>ι : Type u_7<VAR>ι' : Type u_8<VAR>σ : ι ≃ ι'<VAR>f g : M [⋀^ι]→ₗ[R] N<GOAL>AlternatingMap.domDomCongr σ f = AlternatingMap.domDomCongr σ g ↔ f = g
<VAR>R : Type u_1<VAR>Semiring 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>ι : Type u_7<VAR>ι' : Type u_8<VAR>σ : ι ≃ ι'<VAR>f : M [⋀^ι]→ₗ[R] N<GOAL>AlternatingMap.domDomCongr σ f = 0 ↔ f = 0
<VAR>R : Type u_1<VAR>Semiring R<VAR>M : Type u_2<VAR>AddCommMonoid M<VAR>Module R M<VAR>N' : Type u_6<VAR>AddCommGroup N'<VAR>Module R N'<VAR>ι : Type u_7<VAR>g : M [⋀^ι]→ₗ[R] N'<VAR>Fintype ι<VAR>DecidableEq ι<VAR>σ : Equiv.Perm ι<GOAL>AlternatingMap.domDomCongr σ g = Equiv.Perm.sign σ • g
<VAR>R : Type u_1<VAR>Semiring 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>ι : Type u_7<VAR>ι' : Type u_8<VAR>f : M [⋀^ι]→ₗ[R] N<VAR>σ : ι ≃ ι'<GOAL>↑(AlternatingMap.domDomCongr σ f) = MultilinearMap.domDomCongr σ ↑f
<VAR>ι : Type u_7<VAR>K : Type u_12<VAR>Ring K<VAR>M : Type u_13<VAR>AddCommGroup M<VAR>Module K M<VAR>N : Type u_14<VAR>AddCommGroup N<VAR>Module K N<VAR>NoZeroSMulDivisors K N<VAR>f : M [⋀^ι]→ₗ[K] N<VAR>v : ι → M<VAR>h : ¬LinearIndependent K v<GOAL>f v = 0
<VAR>R : Type u_1<VAR>Semiring 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>n : ℕ<VAR>f : M [⋀^Fin n.succ]→ₗ[R] N<VAR>m : Fin n → M<VAR>x y : M<GOAL>f (Matrix.vecCons (x + y) m) = f (Matrix.vecCons x m) + f (Matrix.vecCons y m)
<VAR>R : Type u_1<VAR>Semiring 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>n : ℕ<VAR>f : M [⋀^Fin n.succ]→ₗ[R] N<VAR>m : Fin n → M<VAR>c : R<VAR>x : M<GOAL>f (Matrix.vecCons (c • x) m) = c • f (Matrix.vecCons x m)
<VAR>R : Type u_1<VAR>Semiring R<VAR>M : Type u_2<VAR>AddCommMonoid M<VAR>Module R M<VAR>N' : Type u_6<VAR>AddCommGroup N'<VAR>Module R N'<VAR>ι : Type u_7<VAR>Fintype ι<VAR>DecidableEq ι<VAR>m : MultilinearMap R (fun x => M) N'<VAR>v : ι → M<VAR>i j : ι<VAR>i_ne_j : i ≠ j<VAR>hv : v i = v j<GOAL>(∑ σ : Equiv.Perm ι, Equiv.Perm.sign σ • MultilinearMap.domDomCongr σ m) v = 0
<VAR>R : Type u_1<VAR>Semiring R<VAR>M : Type u_2<VAR>AddCommMonoid M<VAR>Module R M<VAR>N' : Type u_6<VAR>AddCommGroup N'<VAR>Module R N'<VAR>ι : Type u_7<VAR>Fintype ι<VAR>DecidableEq ι<VAR>m : MultilinearMap R (fun x => M) N'<GOAL>⇑(MultilinearMap.alternatization m) = ⇑(∑ σ : Equiv.Perm ι, Equiv.Perm.sign σ • MultilinearMap.domDomCongr σ m)
<VAR>R : Type u_1<VAR>Semiring R<VAR>M : Type u_2<VAR>AddCommMonoid M<VAR>Module R M<VAR>N' : Type u_6<VAR>AddCommGroup N'<VAR>Module R N'<VAR>ι : Type u_7<VAR>Fintype ι<VAR>DecidableEq ι<VAR>m : MultilinearMap R (fun x => M) N'<GOAL>↑(MultilinearMap.alternatization m) = ∑ σ : Equiv.Perm ι, Equiv.Perm.sign σ • MultilinearMap.domDomCongr σ m
<VAR>R : Type u_1<VAR>Semiring R<VAR>M : Type u_2<VAR>AddCommMonoid M<VAR>Module R M<VAR>N' : Type u_6<VAR>AddCommGroup N'<VAR>Module R N'<VAR>ι : Type u_7<VAR>Fintype ι<VAR>DecidableEq ι<VAR>m : MultilinearMap R (fun x => M) N'<VAR>v : ι → M<GOAL>(MultilinearMap.alternatization m) v = ∑ σ : Equiv.Perm ι, Equiv.Perm.sign σ • (MultilinearMap.domDomCongr σ m) v
<VAR>R : Type u_1<VAR>Semiring R<VAR>M : Type u_2<VAR>AddCommMonoid M<VAR>Module R M<VAR>N' : Type u_6<VAR>AddCommGroup N'<VAR>Module R N'<VAR>ι : Type u_7<VAR>DecidableEq ι<VAR>Fintype ι<VAR>a : M [⋀^ι]→ₗ[R] N'<GOAL>MultilinearMap.alternatization ↑a = (Fintype.card ι).factorial • a
<VAR>R : Type u_1<VAR>Semiring R<VAR>M : Type u_2<VAR>AddCommMonoid M<VAR>Module R M<VAR>N' : Type u_6<VAR>AddCommGroup N'<VAR>Module R N'<VAR>ι : Type u_7<VAR>N'₂ : Type u_10<VAR>AddCommGroup N'₂<VAR>Module R N'₂<VAR>DecidableEq ι<VAR>Fintype ι<VAR>g : N' →ₗ[R] N'₂<VAR>f : MultilinearMap R (fun x => M) N'<GOAL>MultilinearMap.alternatization (g.compMultilinearMap f) = g.compAlternatingMap (MultilinearMap.alternatization f)
<VAR>ι : Type u_7<VAR>ι₁ : Type u_10<VAR>Finite ι<VAR>R' : Type u_11<VAR>N₁ : Type u_12<VAR>N₂ : Type u_13<VAR>CommSemiring R'<VAR>AddCommMonoid N₁<VAR>AddCommMonoid N₂<VAR>Module R' N₁<VAR>Module R' N₂<VAR>f g : N₁ [⋀^ι]→ₗ[R'] N₂<VAR>e : Basis ι₁ R' N₁<VAR>h : ∀ (v : ι → ι₁), Function.Injective v → (f fun i => e (v i)) = g fun i => e (v i)<GOAL>f = g
<VAR>R' : Type u_10<VAR>M'' : Type u_11<VAR>N'' : Type u_13<VAR>CommSemiring R'<VAR>AddCommMonoid M''<VAR>AddCommMonoid N''<VAR>Module R' M''<VAR>Module R' N''<VAR>n : ℕ<VAR>f : M'' [⋀^Fin n.succ]→ₗ[R'] N''<VAR>m : M''<VAR>v : Fin n → M''<GOAL>(f.curryLeft m) v = f (Matrix.vecCons m v)
<VAR>R' : Type u_10<VAR>M'' : Type u_11<VAR>N'' : Type u_13<VAR>CommSemiring R'<VAR>AddCommMonoid M''<VAR>AddCommMonoid N''<VAR>Module R' M''<VAR>Module R' N''<VAR>n : ℕ<GOAL>AlternatingMap.curryLeft 0 = 0
<VAR>R' : Type u_10<VAR>M'' : Type u_11<VAR>N'' : Type u_13<VAR>CommSemiring R'<VAR>AddCommMonoid M''<VAR>AddCommMonoid N''<VAR>Module R' M''<VAR>Module R' N''<VAR>n : ℕ<VAR>f g : M'' [⋀^Fin n.succ]→ₗ[R'] N''<GOAL>(f + g).curryLeft = f.curryLeft + g.curryLeft
<VAR>R' : Type u_10<VAR>M'' : Type u_11<VAR>N'' : Type u_13<VAR>CommSemiring R'<VAR>AddCommMonoid M''<VAR>AddCommMonoid N''<VAR>Module R' M''<VAR>Module R' N''<VAR>n : ℕ<VAR>r : R'<VAR>f : M'' [⋀^Fin n.succ]→ₗ[R'] N''<GOAL>(r • f).curryLeft = r • f.curryLeft
<VAR>R' : Type u_10<VAR>M'' : Type u_11<VAR>N'' : Type u_13<VAR>CommSemiring R'<VAR>AddCommMonoid M''<VAR>AddCommMonoid N''<VAR>Module R' M''<VAR>Module R' N''<VAR>n : ℕ<VAR>f : M'' [⋀^Fin n.succ]→ₗ[R'] N''<GOAL>AlternatingMap.curryLeftLinearMap f = f.curryLeft
<VAR>R' : Type u_10<VAR>M'' : Type u_11<VAR>N'' : Type u_13<VAR>CommSemiring R'<VAR>AddCommMonoid M''<VAR>AddCommMonoid N''<VAR>Module R' M''<VAR>Module R' N''<VAR>n : ℕ<VAR>f : M'' [⋀^Fin n.succ.succ]→ₗ[R'] N''<VAR>m : M''<GOAL>(f.curryLeft m).curryLeft m = 0
<VAR>R' : Type u_10<VAR>M'' : Type u_11<VAR>N'' : Type u_13<VAR>N₂'' : Type u_14<VAR>CommSemiring R'<VAR>AddCommMonoid M''<VAR>AddCommMonoid N''<VAR>AddCommMonoid N₂''<VAR>Module R' M''<VAR>Module R' N''<VAR>Module R' N₂''<VAR>n : ℕ<VAR>g : N'' →ₗ[R'] N₂''<VAR>f : M'' [⋀^Fin n.succ]→ₗ[R'] N''<VAR>m : M''<GOAL>(g.compAlternatingMap f).curryLeft m = g.compAlternatingMap (f.curryLeft m)
<VAR>R' : Type u_10<VAR>M'' : Type u_11<VAR>M₂'' : Type u_12<VAR>N'' : Type u_13<VAR>CommSemiring R'<VAR>AddCommMonoid M''<VAR>AddCommMonoid M₂''<VAR>AddCommMonoid N''<VAR>Module R' M''<VAR>Module R' M₂''<VAR>Module R' N''<VAR>n : ℕ<VAR>g : M₂'' →ₗ[R'] M''<VAR>f : M'' [⋀^Fin n.succ]→ₗ[R'] N''<VAR>m : M₂''<GOAL>(f.compLinearMap g).curryLeft m = (f.curryLeft (g m)).compLinearMap g
<VAR>ι : Type u_7<VAR>R' : Type u_10<VAR>M'' : Type u_11<VAR>N'' : Type u_13<VAR>CommSemiring R'<VAR>AddCommMonoid M''<VAR>AddCommMonoid N''<VAR>Module R' M''<VAR>Module R' N''<VAR>IsEmpty ι<VAR>f : M'' [⋀^ι]→ₗ[R'] N''<GOAL>AlternatingMap.constLinearEquivOfIsEmpty.symm f = f 0
<VAR>ι : Type u_7<VAR>R' : Type u_10<VAR>M'' : Type u_11<VAR>N'' : Type u_13<VAR>CommSemiring R'<VAR>AddCommMonoid M''<VAR>AddCommMonoid N''<VAR>Module R' M''<VAR>Module R' N''<VAR>IsEmpty ι<VAR>m : N''<GOAL>AlternatingMap.constLinearEquivOfIsEmpty m = AlternatingMap.constOfIsEmpty R' M'' ι m
<VAR>k : Type u<VAR>Field k<VAR>s : Finset (AlgebraicClosure.MonicIrreducible k)<VAR>f : AlgebraicClosure.MonicIrreducible k<VAR>hf : f ∈ s<GOAL>(AlgebraicClosure.toSplittingField k s) (AlgebraicClosure.evalXSelf k f) = 0
<VAR>k : Type u<VAR>Field k<GOAL>AlgebraicClosure.spanEval k ≠ ⊤
<VAR>k : Type u<VAR>Field k<GOAL>AlgebraicClosure.spanEval k ≤ AlgebraicClosure.maxIdeal k
<VAR>k : Type u<VAR>Field k<GOAL>algebraMap k (AlgebraicClosure.AdjoinMonic k) = (Ideal.Quotient.mk (AlgebraicClosure.maxIdeal k)).comp MvPolynomial.C
<VAR>k : Type u<VAR>Field k<VAR>z : AlgebraicClosure.AdjoinMonic k<GOAL>IsIntegral k z
<VAR>k : Type u<VAR>Field k<VAR>f : k[X]<VAR>hfm : f.Monic<VAR>hfi : Irreducible f<GOAL>∃ x, Polynomial.eval₂ (AlgebraicClosure.toAdjoinMonic k) x f = 0
<VAR>k : Type u<VAR>Field k<GOAL>AlgebraicClosure.Step k 0 = k
<VAR>k : Type u<VAR>Field k<VAR>n : ℕ<GOAL>AlgebraicClosure.Step k (n + 1) = AlgebraicClosure.AdjoinMonic (AlgebraicClosure.Step k n)
<VAR>k : Type u<VAR>Field k<VAR>n : ℕ<VAR>f : (AlgebraicClosure.Step k n)[X]<VAR>hfm : f.Monic<VAR>hfi : Irreducible f<GOAL>∃ x, Polynomial.eval₂ (AlgebraicClosure.toStepSucc k n) x f = 0
<VAR>k : Type u<VAR>Field k<VAR>m n : ℕ<VAR>h : m ≤ n<GOAL>AlgebraicClosure.toStepOfLE' k m n.succ ⋯ = ⇑(AlgebraicClosure.toStepSucc k n) ∘ AlgebraicClosure.toStepOfLE' k m n h
<VAR>k : Type u<VAR>Field k<VAR>m n : ℕ<VAR>h : m ≤ n<GOAL>⇑(AlgebraicClosure.toStepOfLE k m n h) = fun a => Nat.leRecOn h (fun n => ⇑(AlgebraicClosure.toStepSucc k n)) a
<VAR>k : Type u<VAR>Field k<VAR>n : ℕ<VAR>h : 0 ≤ n<GOAL>AlgebraicClosure.toStepOfLE k 0 (n + 1) ⋯ = (AlgebraicClosure.toStepSucc k n).comp (AlgebraicClosure.toStepOfLE k 0 n h)
<VAR>k : Type u<VAR>Field k<VAR>n : ℕ<VAR>z : AlgebraicClosure.Step k n<GOAL>IsIntegral k z
<VAR>k : Type u<VAR>Field k<VAR>n : ℕ<GOAL>(AlgebraicClosureAux.ofStep k (n + 1)).comp (AlgebraicClosure.toStepSucc k n) = AlgebraicClosureAux.ofStep k n
<VAR>k : Type u<VAR>Field k<VAR>z : AlgebraicClosureAux k<GOAL>∃ n x, (AlgebraicClosureAux.ofStep k n) x = z
<VAR>k : Type u<VAR>Field k<VAR>f : (AlgebraicClosureAux k)[X]<VAR>hfm : f.Monic<VAR>hfi : Irreducible f<GOAL>∃ x, Polynomial.eval x f = 0
<VAR>k : Type u<VAR>Field k<GOAL>IsAlgClosed (AlgebraicClosureAux k)
<VAR>k : Type u<VAR>Field k<GOAL>IsAlgClosure k (AlgebraicClosureAux k)
<VAR>K : Type v<VAR>L : Type w<VAR>Field K<VAR>Field L<VAR>Algebra K L<VAR>f : K[X]<VAR>self : Polynomial.IsSplittingField K L f<GOAL>Algebra.adjoin K (f.rootSet L) = ⊤
<VAR>K : Type v<VAR>L : Type w<VAR>Field K<VAR>Field L<VAR>Algebra K L<VAR>f : K[X]<VAR>self : Polynomial.IsSplittingField K L f<GOAL>Polynomial.Splits (algebraMap K L) f
<VAR>K : Type v<VAR>L : Type w<VAR>Field K<VAR>Field L<VAR>Algebra K L<VAR>f : K[X]<VAR>Polynomial.IsSplittingField K L f<GOAL>Polynomial.Splits (algebraMap K L) f
<VAR>K : Type v<VAR>L : Type w<VAR>Field K<VAR>Field L<VAR>Algebra K L<VAR>f : K[X]<VAR>Polynomial.IsSplittingField K L f<GOAL>Algebra.adjoin K (f.rootSet L) = ⊤
<VAR>K : Type v<VAR>L : Type w<VAR>Field K<VAR>Field L<VAR>Algebra K L<VAR>f : K[X]<VAR>Polynomial.IsSplittingField K L f<GOAL>Polynomial.Splits (RingHom.id K) f ↔ ⊤ = ⊥
<VAR>F : Type u<VAR>K : Type v<VAR>L : Type w<VAR>Field K<VAR>Field L<VAR>Field F<VAR>Algebra K L<VAR>Algebra F K<VAR>Algebra F L<VAR>IsScalarTower F K L<VAR>f g : F[X]<VAR>hf : f ≠ 0<VAR>hg : g ≠ 0<VAR>Polynomial.IsSplittingField F K f<VAR>Polynomial.IsSplittingField K L (Polynomial.map (algebraMap F K) g)<GOAL>Polynomial.IsSplittingField F L (f * g)
<VAR>K : Type v<VAR>L : Type w<VAR>Field K<VAR>Field L<VAR>Algebra K L<VAR>f : K[X]<VAR>Polynomial.IsSplittingField K L f<GOAL>FiniteDimensional K L
<VAR>F : Type u<VAR>K : Type v<VAR>L : Type w<VAR>Field K<VAR>Field L<VAR>Field F<VAR>Algebra K L<VAR>Algebra K F<VAR>p : K[X]<VAR>f : F ≃ₐ[K] L<VAR>Polynomial.IsSplittingField K F p<GOAL>Polynomial.IsSplittingField K L p
<VAR>F : Type u<VAR>K : Type v<VAR>L : Type w<VAR>Field K<VAR>Field L<VAR>Field F<VAR>Algebra K L<VAR>Algebra K F<VAR>f : K[X]<VAR>Polynomial.IsSplittingField K L f<VAR>i : L →ₐ[K] F<GOAL>Algebra.adjoin K (f.rootSet F) = i.range
<VAR>K : Type v<VAR>L : Type w<VAR>Field K<VAR>Field L<VAR>Algebra K L<VAR>p : K[X]<VAR>F : IntermediateField K L<VAR>h : Polynomial.Splits (algebraMap K L) p<VAR>hF : ∀ x ∈ p.rootSet L, x ∈ F<GOAL>Polynomial.Splits (algebraMap K ↥F) p
<VAR>K : Type v<VAR>L : Type w<VAR>Field K<VAR>Field L<VAR>Algebra K L<VAR>x : L<VAR>int : IsIntegral K x<VAR>F : IntermediateField K L<VAR>h : Polynomial.Splits (algebraMap K ↥F) (minpoly K x)<GOAL>x ∈ F
<VAR>σ : Type u<VAR>K : Type v<VAR>Field K<VAR>I : Ideal (MvPolynomial σ K)<VAR>hI : I ≠ ⊤<GOAL>Function.Injective ⇑((Ideal.Quotient.mk I).comp MvPolynomial.C)
<VAR>σ K : Type u<VAR>Field K<GOAL>Module.rank K (MvPolynomial σ K) = Cardinal.mk (σ →₀ ℕ)
<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>CommSemiring R₁<VAR>AddCommMonoid M₁<VAR>Module R₁ M₁<VAR>CommSemiring R₂<VAR>AddCommMonoid M₂<VAR>Module R₂ M₂<VAR>AddCommMonoid M<VAR>Module R M<VAR>I₁ : R₁ →+* R<VAR>I₂ : R₂ →+* R<VAR>B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] M<VAR>x : M₁<VAR>y : M₂<GOAL>B.IsOrtho x y ↔ (B x) 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>CommSemiring R₁<VAR>AddCommMonoid M₁<VAR>Module R₁ M₁<VAR>CommSemiring R₂<VAR>AddCommMonoid M₂<VAR>Module R₂ M₂<VAR>AddCommMonoid M<VAR>Module R M<VAR>I₁ : R₁ →+* R<VAR>I₂ : R₂ →+* R<VAR>B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] M<VAR>x : M₂<GOAL>B.IsOrtho 0 x
<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>CommSemiring R₁<VAR>AddCommMonoid M₁<VAR>Module R₁ M₁<VAR>CommSemiring R₂<VAR>AddCommMonoid M₂<VAR>Module R₂ M₂<VAR>AddCommMonoid M<VAR>Module R M<VAR>I₁ : R₁ →+* R<VAR>I₂ : R₂ →+* R<VAR>B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] M<VAR>x : M₁<GOAL>B.IsOrtho x 0
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>M : Type u_5<VAR>M₁ : Type u_6<VAR>CommSemiring R<VAR>CommSemiring R₁<VAR>AddCommMonoid M₁<VAR>Module R₁ M₁<VAR>AddCommMonoid M<VAR>Module R M<VAR>I₁ I₁' : R₁ →+* R<VAR>B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₁'] M<VAR>x y : M₁<GOAL>B.IsOrtho x y ↔ B.flip.IsOrtho y x
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>M : Type u_5<VAR>M₁ : Type u_6<VAR>n : Type u_19<VAR>CommSemiring R<VAR>CommSemiring R₁<VAR>AddCommMonoid M₁<VAR>Module R₁ M₁<VAR>AddCommMonoid M<VAR>Module R M<VAR>I₁ I₁' : R₁ →+* R<VAR>B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₁'] M<VAR>v : n → M₁<GOAL>B.IsOrthoᵢ v ↔ ∀ (i j : n), i ≠ j → (B (v i)) (v j) = 0
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>M : Type u_5<VAR>M₁ : Type u_6<VAR>n : Type u_19<VAR>CommSemiring R<VAR>CommSemiring R₁<VAR>AddCommMonoid M₁<VAR>Module R₁ M₁<VAR>AddCommMonoid M<VAR>Module R M<VAR>I₁ I₁' : R₁ →+* R<VAR>B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₁'] M<VAR>v : n → M₁<GOAL>B.IsOrthoᵢ v ↔ B.flip.IsOrthoᵢ v
<VAR>K : Type u_13<VAR>K₁ : Type u_14<VAR>K₂ : Type u_15<VAR>V : Type u_16<VAR>V₁ : Type u_17<VAR>V₂ : Type u_18<VAR>Field K<VAR>AddCommGroup V<VAR>Module K V<VAR>Field K₁<VAR>AddCommGroup V₁<VAR>Module K₁ V₁<VAR>Field K₂<VAR>AddCommGroup V₂<VAR>Module K₂ V₂<VAR>I₁ : K₁ →+* K<VAR>I₂ : K₂ →+* K<VAR>B : V₁ →ₛₗ[I₁] V₂ →ₛₗ[I₂] V<VAR>x : V₁<VAR>y : V₂<VAR>a : K₁<VAR>ha : a ≠ 0<GOAL>B.IsOrtho x y ↔ B.IsOrtho (a • x) y
<VAR>K : Type u_13<VAR>K₁ : Type u_14<VAR>K₂ : Type u_15<VAR>V : Type u_16<VAR>V₁ : Type u_17<VAR>V₂ : Type u_18<VAR>Field K<VAR>AddCommGroup V<VAR>Module K V<VAR>Field K₁<VAR>AddCommGroup V₁<VAR>Module K₁ V₁<VAR>Field K₂<VAR>AddCommGroup V₂<VAR>Module K₂ V₂<VAR>I₁ : K₁ →+* K<VAR>I₂ : K₂ →+* K<VAR>B : V₁ →ₛₗ[I₁] V₂ →ₛₗ[I₂] V<VAR>x : V₁<VAR>y : V₂<VAR>a : K₂<VAR>ha : a ≠ 0<GOAL>B.IsOrtho x y ↔ B.IsOrtho x (a • y)
<VAR>K : Type u_13<VAR>K₁ : Type u_14<VAR>V : Type u_16<VAR>V₁ : Type u_17<VAR>n : Type u_19<VAR>Field K<VAR>AddCommGroup V<VAR>Module K V<VAR>Field K₁<VAR>AddCommGroup V₁<VAR>Module K₁ V₁<VAR>I₁ I₁' : K₁ →+* K<VAR>B : V₁ →ₛₗ[I₁] V₁ →ₛₗ[I₁'] V<VAR>v : n → V₁<VAR>hv₁ : B.IsOrthoᵢ v<VAR>hv₂ : ∀ (i : n), ¬B.IsOrtho (v i) (v i)<GOAL>LinearIndependent K₁ v
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>M : Type u_5<VAR>M₁ : Type u_6<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>CommSemiring R₁<VAR>AddCommMonoid M₁<VAR>Module R₁ M₁<VAR>I₁ I₂ : R₁ →+* R<VAR>B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] M<VAR>H : B.IsRefl<VAR>x y : M₁<GOAL>(B x) y = 0 → (B y) x = 0
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>M : Type u_5<VAR>M₁ : Type u_6<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>CommSemiring R₁<VAR>AddCommMonoid M₁<VAR>Module R₁ M₁<VAR>I₁ I₂ : R₁ →+* R<VAR>B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] M<VAR>H : B.IsRefl<VAR>x y : M₁<GOAL>B.IsOrtho x y ↔ B.IsOrtho y x
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>M : Type u_5<VAR>M₁ : Type u_6<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>CommSemiring R₁<VAR>AddCommMonoid M₁<VAR>Module R₁ M₁<VAR>I₁ I₂ : R₁ →+* R<VAR>B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] M<VAR>H : B.IsRefl<VAR>p : Submodule R₁ M₁<GOAL>(B.domRestrict₁₂ p p).IsRefl
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>M : Type u_5<VAR>M₁ : Type u_6<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>CommSemiring R₁<VAR>AddCommMonoid M₁<VAR>Module R₁ M₁<VAR>I₁ I₂ : R₁ →+* R<VAR>B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] M<GOAL>B.flip.IsRefl ↔ B.IsRefl
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>M : Type u_5<VAR>M₁ : Type u_6<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>CommSemiring R₁<VAR>AddCommMonoid M₁<VAR>Module R₁ M₁<VAR>I₁ I₂ : R₁ →+* R<VAR>B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] M<VAR>H : B.IsRefl<VAR>h : LinearMap.ker B = ⊥<GOAL>LinearMap.ker B.flip = ⊥
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>M : Type u_5<VAR>M₁ : Type u_6<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>CommSemiring R₁<VAR>AddCommMonoid M₁<VAR>Module R₁ M₁<VAR>I₁ I₂ : R₁ →+* R<VAR>B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] M<VAR>H : B.IsRefl<GOAL>LinearMap.ker B = ⊥ ↔ LinearMap.ker B.flip = ⊥
<VAR>R : Type u_1<VAR>M : Type u_5<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>I : R →+* R<VAR>B : M →ₛₗ[I] M →ₗ[R] R<VAR>H : B.IsSymm<VAR>x y : M<GOAL>I ((B x) y) = (B y) x
<VAR>R : Type u_1<VAR>M : Type u_5<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>I : R →+* R<VAR>B : M →ₛₗ[I] M →ₗ[R] R<VAR>H : B.IsSymm<GOAL>B.IsRefl
<VAR>R : Type u_1<VAR>M : Type u_5<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>I : R →+* R<VAR>B : M →ₛₗ[I] M →ₗ[R] R<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_5<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>I : R →+* R<VAR>B : M →ₛₗ[I] M →ₗ[R] R<VAR>H : B.IsSymm<VAR>p : Submodule R M<GOAL>(B.domRestrict₁₂ p p).IsSymm
<VAR>R : Type u_1<VAR>M : Type u_5<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>I : R →+* R<GOAL>LinearMap.IsSymm 0
<VAR>R : Type u_1<VAR>M : Type u_5<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>B : LinearMap.BilinForm R M<GOAL>LinearMap.IsSymm B ↔ B = LinearMap.flip B
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>M : Type u_5<VAR>M₁ : Type u_6<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>CommSemiring R₁<VAR>AddCommMonoid M₁<VAR>Module R₁ M₁<VAR>I₁ I₂ : R₁ →+* R<VAR>B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] M<VAR>H : B.IsAlt<VAR>x : M₁<GOAL>(B x) x = 0
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>M : Type u_5<VAR>M₁ : Type u_6<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>CommSemiring R₁<VAR>AddCommMonoid M₁<VAR>Module R₁ M₁<VAR>I₁ I₂ : R₁ →+* R<VAR>B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] M<VAR>H : B.IsAlt<VAR>IsCancelAdd M<VAR>a b c : M₁<VAR>hAdd : a + b + c = 0<GOAL>(B a) b = (B b) c
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>M : Type u_5<VAR>M₁ : Type u_6<VAR>CommSemiring R<VAR>AddCommGroup M<VAR>Module R M<VAR>CommSemiring R₁<VAR>AddCommMonoid M₁<VAR>Module R₁ M₁<VAR>I₁ I₂ : R₁ →+* R<VAR>B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] M<VAR>H : B.IsAlt<VAR>x y : M₁<GOAL>-(B x) y = (B y) x
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>M : Type u_5<VAR>M₁ : Type u_6<VAR>CommSemiring R<VAR>AddCommGroup M<VAR>Module R M<VAR>CommSemiring R₁<VAR>AddCommMonoid M₁<VAR>Module R₁ M₁<VAR>I₁ I₂ : R₁ →+* R<VAR>B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] M<VAR>H : B.IsAlt<GOAL>B.IsRefl
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>M : Type u_5<VAR>M₁ : Type u_6<VAR>CommSemiring R<VAR>AddCommGroup M<VAR>Module R M<VAR>CommSemiring R₁<VAR>AddCommMonoid M₁<VAR>Module R₁ M₁<VAR>I₁ I₂ : R₁ →+* R<VAR>B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] M<VAR>H : B.IsAlt<VAR>x y : M₁<GOAL>B.IsOrtho x y ↔ B.IsOrtho y x
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>M₁ : Type u_6<VAR>CommRing R<VAR>CommSemiring R₁<VAR>AddCommMonoid M₁<VAR>Module R₁ M₁<VAR>I : R₁ →+* R<VAR>NoZeroDivisors R<VAR>CharZero R<VAR>B : M₁ →ₛₗ[I] M₁ →ₛₗ[I] R<GOAL>B.IsAlt ↔ B = -B.flip
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>M : Type u_5<VAR>M₁ : Type u_6<VAR>CommRing R<VAR>CommRing R₁<VAR>AddCommGroup M₁<VAR>Module R₁ M₁<VAR>AddCommGroup M<VAR>Module R M<VAR>I₁ I₂ : R₁ →+* R<VAR>B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] M<VAR>N : Submodule R₁ M₁<VAR>m : M₁<GOAL>m ∈ N.orthogonalBilin B ↔ ∀ n ∈ N, B.IsOrtho n m
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>M : Type u_5<VAR>M₁ : Type u_6<VAR>CommRing R<VAR>CommRing R₁<VAR>AddCommGroup M₁<VAR>Module R₁ M₁<VAR>AddCommGroup M<VAR>Module R M<VAR>I₁ I₂ : R₁ →+* R<VAR>B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] M<VAR>N L : Submodule R₁ M₁<VAR>h : N ≤ L<GOAL>L.orthogonalBilin B ≤ N.orthogonalBilin B
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>M : Type u_5<VAR>M₁ : Type u_6<VAR>CommRing R<VAR>CommRing R₁<VAR>AddCommGroup M₁<VAR>Module R₁ M₁<VAR>AddCommGroup M<VAR>Module R M<VAR>I₁ I₂ : R₁ →+* R<VAR>B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] M<VAR>N : Submodule R₁ M₁<VAR>b : B.IsRefl<GOAL>N ≤ (N.orthogonalBilin B).orthogonalBilin B
<VAR>K : Type u_13<VAR>K₁ : Type u_14<VAR>V₁ : Type u_17<VAR>V₂ : Type u_18<VAR>Field K<VAR>Field K₁<VAR>AddCommGroup V₁<VAR>Module K₁ V₁<VAR>AddCommGroup V₂<VAR>Module K V₂<VAR>J₁ J₁' : K₁ →+* K<VAR>B : V₁ →ₛₗ[J₁] V₁ →ₛₗ[J₁'] V₂<VAR>x : V₁<VAR>hx : ¬B.IsOrtho x x<GOAL>Submodule.span K₁ {x} ⊓ (Submodule.span K₁ {x}).orthogonalBilin B = ⊥
<VAR>K : Type u_13<VAR>V : Type u_16<VAR>V₂ : Type u_18<VAR>Field K<VAR>AddCommGroup V<VAR>Module K V<VAR>AddCommGroup V₂<VAR>Module K V₂<VAR>J : K →+* K<VAR>B : V →ₗ[K] V →ₛₗ[J] V₂<VAR>x : V<GOAL>(Submodule.span K {x}).orthogonalBilin B = LinearMap.ker (B x)
<VAR>K : Type u_13<VAR>V : Type u_16<VAR>Field K<VAR>AddCommGroup V<VAR>Module K V<VAR>B : V →ₗ[K] V →ₗ[K] K<VAR>x : V<VAR>hx : ¬B.IsOrtho x x<GOAL>Submodule.span K {x} ⊔ (Submodule.span K {x}).orthogonalBilin B = ⊤
<VAR>K : Type u_13<VAR>V : Type u_16<VAR>Field K<VAR>AddCommGroup V<VAR>Module K V<VAR>B : V →ₗ[K] V →ₗ[K] K<VAR>x : V<VAR>hx : ¬B.IsOrtho x x<GOAL>IsCompl (Submodule.span K {x}) ((Submodule.span K {x}).orthogonalBilin B)