ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>V : Type u_3<VAR>CommRing R<VAR>CommRing A<VAR>AddCommGroup V<VAR>Algebra R A<VAR>Module R V<VAR>Invertible 2<VAR>Q : QuadraticForm R V<VAR>a : CliffordAlgebra (QuadraticForm.baseChange A Q)<GOAL>(CliffordAlgebra.equivBaseChange A Q) a = (CliffordAlgebra.toBaseChange A Q) a
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>V : Type u_3<VAR>CommRing R<VAR>CommRing A<VAR>AddCommGroup V<VAR>Algebra R A<VAR>Module R V<VAR>Invertible 2<VAR>Q : QuadraticForm R V<VAR>a : A ⊗[R] CliffordAlgebra Q<GOAL>(CliffordAlgebra.equivBaseChange A Q).symm a = (CliffordAlgebra.ofBaseChange A Q) a
<VAR>R : Type uR<VAR>M : Type uM<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>Q : QuadraticForm R M<GOAL>Subalgebra.toSubmodule (CliffordAlgebra.even Q) = CliffordAlgebra.evenOdd Q 0
<VAR>R : Type uR<VAR>M : Type uM<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>Q : QuadraticForm R M<VAR>A : Type uA<VAR>Ring A<VAR>Algebra R A<VAR>self : CliffordAlgebra.EvenHom Q A<VAR>m : M<GOAL>(self.bilin m) m = (algebraMap R A) (Q m)
<VAR>R : Type uR<VAR>M : Type uM<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>Q : QuadraticForm R M<VAR>A : Type uA<VAR>Ring A<VAR>Algebra R A<VAR>self : CliffordAlgebra.EvenHom Q A<VAR>m₁ m₂ m₃ : M<GOAL>(self.bilin m₁) m₂ * (self.bilin m₂) m₃ = Q m₂ • (self.bilin m₁) m₃
<VAR>R : Type uR<VAR>M : Type uM<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>Q : QuadraticForm R M<VAR>A : Type uA<VAR>B : Type uB<VAR>Ring A<VAR>Ring B<VAR>Algebra R A<VAR>Algebra R B<VAR>g : CliffordAlgebra.EvenHom Q A<VAR>f : A →ₐ[R] B<GOAL>(g.compr₂ f).bilin = g.bilin.compr₂ f.toLinearMap
<VAR>R : Type uR<VAR>M : Type uM<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>Q : QuadraticForm R M<VAR>A : Type uA<VAR>Ring A<VAR>Algebra R A<VAR>f g : ↥(CliffordAlgebra.even Q) →ₐ[R] A<VAR>h : (CliffordAlgebra.even.ι Q).compr₂ f = (CliffordAlgebra.even.ι Q).compr₂ g<GOAL>f = g
<VAR>R : Type uR<VAR>M : Type uM<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>Q : QuadraticForm R M<VAR>A : Type uA<VAR>Ring A<VAR>Algebra R A<VAR>f : CliffordAlgebra.EvenHom Q A<VAR>m₁ m₂ : M<VAR>x : A × ↥(CliffordAlgebra.even.lift.S f)<GOAL>(((CliffordAlgebra.even.lift.fFold f) m₁) (((CliffordAlgebra.even.lift.fFold f) m₂) x)).1 = (f.bilin m₁) m₂ * x.1
<VAR>R : Type uR<VAR>M : Type uM<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>Q : QuadraticForm R M<VAR>A : Type uA<VAR>Ring A<VAR>Algebra R A<VAR>f : CliffordAlgebra.EvenHom Q A<VAR>m₁ m₂ m₃ : M<VAR>x : A × ↥(CliffordAlgebra.even.lift.S f)<GOAL>↑(((CliffordAlgebra.even.lift.fFold f) m₁) (((CliffordAlgebra.even.lift.fFold f) m₂) x)).2 m₃ = (f.bilin m₃) m₁ * ↑x.2 m₂
<VAR>R : Type uR<VAR>M : Type uM<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>Q : QuadraticForm R M<VAR>A : Type uA<VAR>Ring A<VAR>Algebra R A<VAR>f : CliffordAlgebra.EvenHom Q A<VAR>m : M<VAR>x : A × ↥(CliffordAlgebra.even.lift.S f)<GOAL>((CliffordAlgebra.even.lift.fFold f) m) (((CliffordAlgebra.even.lift.fFold f) m) x) = Q m • x
<VAR>R : Type uR<VAR>M : Type uM<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>Q : QuadraticForm R M<VAR>A : Type uA<VAR>Ring A<VAR>Algebra R A<VAR>f : CliffordAlgebra.EvenHom Q A<GOAL>∀ (a : ↥(CliffordAlgebra.even Q)), (CliffordAlgebra.even.lift.aux f) a = (((CliffordAlgebra.foldr Q (CliffordAlgebra.even.lift.fFold f) ⋯) (1, 0)) ↑a).1
<VAR>R : Type uR<VAR>M : Type uM<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>Q : QuadraticForm R M<VAR>A : Type uA<VAR>Ring A<VAR>Algebra R A<VAR>f : CliffordAlgebra.EvenHom Q A<GOAL>(CliffordAlgebra.even.lift.aux f) 1 = 1
<VAR>R : Type uR<VAR>M : Type uM<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>Q : QuadraticForm R M<VAR>A : Type uA<VAR>Ring A<VAR>Algebra R A<VAR>f : CliffordAlgebra.EvenHom Q A<VAR>m₁ m₂ : M<GOAL>(CliffordAlgebra.even.lift.aux f) (((CliffordAlgebra.even.ι Q).bilin m₁) m₂) = (f.bilin m₁) m₂
<VAR>R : Type uR<VAR>M : Type uM<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>Q : QuadraticForm R M<VAR>A : Type uA<VAR>Ring A<VAR>Algebra R A<VAR>f : CliffordAlgebra.EvenHom Q A<VAR>r : R<VAR>hr : (algebraMap R (CliffordAlgebra Q)) r ∈ CliffordAlgebra.even Q<GOAL>(CliffordAlgebra.even.lift.aux f) ⟨(algebraMap R (CliffordAlgebra Q)) r, hr⟩ = (algebraMap R A) r
<VAR>R : Type uR<VAR>M : Type uM<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>Q : QuadraticForm R M<VAR>A : Type uA<VAR>Ring A<VAR>Algebra R A<VAR>f : CliffordAlgebra.EvenHom Q A<VAR>x y : ↥(CliffordAlgebra.even Q)<GOAL>(CliffordAlgebra.even.lift.aux f) (x * y) = (CliffordAlgebra.even.lift.aux f) x * (CliffordAlgebra.even.lift.aux f) y
<VAR>R : Type uR<VAR>M : Type uM<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>Q : QuadraticForm R M<VAR>A : Type uA<VAR>Ring A<VAR>Algebra R A<VAR>F : ↥(CliffordAlgebra.even Q) →ₐ[R] A<GOAL>((CliffordAlgebra.even.lift Q).symm F).bilin = (CliffordAlgebra.even.ι Q).bilin.compr₂ F.toLinearMap
<VAR>R : Type uR<VAR>M : Type uM<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>Q : QuadraticForm R M<VAR>A : Type uA<VAR>Ring A<VAR>Algebra R A<VAR>f : CliffordAlgebra.EvenHom Q A<VAR>m₁ m₂ : M<GOAL>((CliffordAlgebra.even.lift Q) f) (((CliffordAlgebra.even.ι Q).bilin m₁) m₂) = (f.bilin m₁) m₂
<VAR>R : Type u<VAR>Semiring R<GOAL>StrongRankCondition R ↔ ∀ {n m : ℕ} (f : (Fin n → R) →ₗ[R] Fin m → R), Function.Injective ⇑f → n ≤ m
<VAR>R : Type u<VAR>Semiring R<VAR>self : StrongRankCondition R<VAR>n m : ℕ<VAR>f : (Fin n → R) →ₗ[R] Fin m → R<GOAL>Function.Injective ⇑f → n ≤ m
<VAR>R : Type u<VAR>Semiring R<VAR>StrongRankCondition R<VAR>n m : ℕ<VAR>f : (Fin n → R) →ₗ[R] Fin m → R<GOAL>Function.Injective ⇑f → n ≤ m
<VAR>R : Type u<VAR>Semiring R<GOAL>StrongRankCondition R ↔ ∀ (n : ℕ) (f : (Fin (n + 1) → R) →ₗ[R] Fin n → R), ¬Function.Injective ⇑f
<VAR>R : Type u<VAR>Semiring R<VAR>StrongRankCondition R<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Fintype α<VAR>Fintype β<VAR>f : (α → R) →ₗ[R] β → R<VAR>i : Function.Injective ⇑f<GOAL>Fintype.card α ≤ Fintype.card β
<VAR>R : Type u<VAR>Semiring R<VAR>StrongRankCondition R<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Fintype α<VAR>Fintype β<VAR>f : (α →₀ R) →ₗ[R] β →₀ R<VAR>i : Function.Injective ⇑f<GOAL>Fintype.card α ≤ Fintype.card β
<VAR>R : Type u<VAR>Semiring R<VAR>self : RankCondition R<VAR>n m : ℕ<VAR>f : (Fin n → R) →ₗ[R] Fin m → R<GOAL>Function.Surjective ⇑f → m ≤ n
<VAR>R : Type u<VAR>Semiring R<VAR>RankCondition R<VAR>n m : ℕ<VAR>f : (Fin n → R) →ₗ[R] Fin m → R<GOAL>Function.Surjective ⇑f → m ≤ n
<VAR>R : Type u<VAR>Semiring R<VAR>RankCondition R<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Fintype α<VAR>Fintype β<VAR>f : (α → R) →ₗ[R] β → R<VAR>i : Function.Surjective ⇑f<GOAL>Fintype.card β ≤ Fintype.card α
<VAR>R : Type u<VAR>Semiring R<VAR>RankCondition R<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Fintype α<VAR>Fintype β<VAR>f : (α →₀ R) →ₗ[R] β →₀ R<VAR>i : Function.Surjective ⇑f<GOAL>Fintype.card β ≤ Fintype.card α
<VAR>R : Type u<VAR>Semiring R<VAR>self : InvariantBasisNumber R<VAR>n m : ℕ<GOAL>((Fin n → R) ≃ₗ[R] Fin m → R) → n = m
<VAR>R : Type u<VAR>Semiring R<VAR>InvariantBasisNumber R<VAR>n m : ℕ<GOAL>((Fin n → R) ≃ₗ[R] Fin m → R) → n = m
<VAR>R : Type u<VAR>Semiring R<VAR>InvariantBasisNumber R<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Fintype α<VAR>Fintype β<VAR>f : (α → R) ≃ₗ[R] β → R<GOAL>Fintype.card α = Fintype.card β
<VAR>R : Type u<VAR>Semiring R<VAR>InvariantBasisNumber R<GOAL>Nontrivial R
<VAR>R : Type uR<VAR>M₁ : Type uM₁<VAR>M₂ : Type uM₂<VAR>M₃ : Type uM₃<VAR>M₄ : Type uM₄<VAR>CommRing R<VAR>AddCommGroup M₁<VAR>AddCommGroup M₂<VAR>AddCommGroup M₃<VAR>AddCommGroup M₄<VAR>Module R M₁<VAR>Module R M₂<VAR>Module R M₃<VAR>Module R M₄<VAR>Invertible 2<VAR>Q₁ : QuadraticForm R M₁<VAR>Q₂ : QuadraticForm R M₂<VAR>Q₃ : QuadraticForm R M₃<VAR>Q₄ : QuadraticForm R M₄<VAR>f : Q₁ →qᵢ Q₂<VAR>g : Q₃ →qᵢ Q₄<GOAL>QuadraticMap.comp (Q₂.tmul Q₄) (TensorProduct.map f.toLinearMap g.toLinearMap) = Q₁.tmul Q₃
<VAR>R : Type uR<VAR>M₁ : Type uM₁<VAR>M₂ : Type uM₂<VAR>M₃ : Type uM₃<VAR>M₄ : Type uM₄<VAR>CommRing R<VAR>AddCommGroup M₁<VAR>AddCommGroup M₂<VAR>AddCommGroup M₃<VAR>AddCommGroup M₄<VAR>Module R M₁<VAR>Module R M₂<VAR>Module R M₃<VAR>Module R M₄<VAR>Invertible 2<VAR>Q₁ : QuadraticForm R M₁<VAR>Q₂ : QuadraticForm R M₂<VAR>Q₃ : QuadraticForm R M₃<VAR>Q₄ : QuadraticForm R M₄<VAR>f : Q₁ →qᵢ Q₂<VAR>g : Q₃ →qᵢ Q₄<VAR>x : M₁ ⊗[R] M₃<GOAL>(Q₂.tmul Q₄) ((TensorProduct.map f.toLinearMap g.toLinearMap) x) = (Q₁.tmul Q₃) x
<VAR>R : Type uR<VAR>M₁ : Type uM₁<VAR>M₂ : Type uM₂<VAR>M₃ : Type uM₃<VAR>M₄ : Type uM₄<VAR>CommRing R<VAR>AddCommGroup M₁<VAR>AddCommGroup M₂<VAR>AddCommGroup M₃<VAR>AddCommGroup M₄<VAR>Module R M₁<VAR>Module R M₂<VAR>Module R M₃<VAR>Module R M₄<VAR>Invertible 2<VAR>Q₁ : QuadraticForm R M₁<VAR>Q₂ : QuadraticForm R M₂<VAR>Q₃ : QuadraticForm R M₃<VAR>Q₄ : QuadraticForm R M₄<VAR>f : Q₁ →qᵢ Q₂<VAR>g : Q₃ →qᵢ Q₄<VAR>x : M₁ ⊗[R] M₃<GOAL>(f.tmul g) x = (TensorProduct.map f.toLinearMap g.toLinearMap) x
<VAR>R : Type uR<VAR>M₁ : Type uM₁<VAR>M₂ : Type uM₂<VAR>CommRing R<VAR>AddCommGroup M₁<VAR>AddCommGroup M₂<VAR>Module R M₁<VAR>Module R M₂<VAR>Invertible 2<VAR>Q₁ : QuadraticForm R M₁<VAR>Q₂ : QuadraticForm R M₂<GOAL>QuadraticMap.comp (Q₂.tmul Q₁) ↑(TensorProduct.comm R M₁ M₂) = Q₁.tmul Q₂
<VAR>R : Type uR<VAR>M₁ : Type uM₁<VAR>M₂ : Type uM₂<VAR>CommRing R<VAR>AddCommGroup M₁<VAR>AddCommGroup M₂<VAR>Module R M₁<VAR>Module R M₂<VAR>Invertible 2<VAR>Q₁ : QuadraticForm R M₁<VAR>Q₂ : QuadraticForm R M₂<VAR>x : M₁ ⊗[R] M₂<GOAL>(Q₂.tmul Q₁) ((TensorProduct.comm R M₁ M₂) x) = (Q₁.tmul Q₂) x
<VAR>R : Type uR<VAR>M₁ : Type uM₁<VAR>M₂ : Type uM₂<VAR>CommRing R<VAR>AddCommGroup M₁<VAR>AddCommGroup M₂<VAR>Module R M₁<VAR>Module R M₂<VAR>Invertible 2<VAR>Q₁ : QuadraticForm R M₁<VAR>Q₂ : QuadraticForm R M₂<GOAL>(Q₁.tensorComm Q₂).toLinearEquiv = TensorProduct.comm R M₁ M₂
<VAR>R : Type uR<VAR>M₁ : Type uM₁<VAR>M₂ : Type uM₂<VAR>CommRing R<VAR>AddCommGroup M₁<VAR>AddCommGroup M₂<VAR>Module R M₁<VAR>Module R M₂<VAR>Invertible 2<VAR>Q₁ : QuadraticForm R M₁<VAR>Q₂ : QuadraticForm R M₂<VAR>x : M₁ ⊗[R] M₂<GOAL>(Q₁.tensorComm Q₂) x = (TensorProduct.comm R M₁ M₂) x
<VAR>R : Type uR<VAR>M₁ : Type uM₁<VAR>M₂ : Type uM₂<VAR>CommRing R<VAR>AddCommGroup M₁<VAR>AddCommGroup M₂<VAR>Module R M₁<VAR>Module R M₂<VAR>Invertible 2<VAR>Q₁ : QuadraticForm R M₁<VAR>Q₂ : QuadraticForm R M₂<GOAL>(Q₁.tensorComm Q₂).symm = Q₂.tensorComm Q₁
<VAR>R : Type uR<VAR>M₁ : Type uM₁<VAR>M₂ : Type uM₂<VAR>M₃ : Type uM₃<VAR>CommRing R<VAR>AddCommGroup M₁<VAR>AddCommGroup M₂<VAR>AddCommGroup M₃<VAR>Module R M₁<VAR>Module R M₂<VAR>Module R M₃<VAR>Invertible 2<VAR>Q₁ : QuadraticForm R M₁<VAR>Q₂ : QuadraticForm R M₂<VAR>Q₃ : QuadraticForm R M₃<GOAL>QuadraticMap.comp (Q₁.tmul (Q₂.tmul Q₃)) ↑(TensorProduct.assoc R M₁ M₂ M₃) = (Q₁.tmul Q₂).tmul Q₃
<VAR>R : Type uR<VAR>M₁ : Type uM₁<VAR>M₂ : Type uM₂<VAR>M₃ : Type uM₃<VAR>CommRing R<VAR>AddCommGroup M₁<VAR>AddCommGroup M₂<VAR>AddCommGroup M₃<VAR>Module R M₁<VAR>Module R M₂<VAR>Module R M₃<VAR>Invertible 2<VAR>Q₁ : QuadraticForm R M₁<VAR>Q₂ : QuadraticForm R M₂<VAR>Q₃ : QuadraticForm R M₃<VAR>x : (M₁ ⊗[R] M₂) ⊗[R] M₃<GOAL>(Q₁.tmul (Q₂.tmul Q₃)) ((TensorProduct.assoc R M₁ M₂ M₃) x) = ((Q₁.tmul Q₂).tmul Q₃) x
<VAR>R : Type uR<VAR>M₁ : Type uM₁<VAR>M₂ : Type uM₂<VAR>M₃ : Type uM₃<VAR>CommRing R<VAR>AddCommGroup M₁<VAR>AddCommGroup M₂<VAR>AddCommGroup M₃<VAR>Module R M₁<VAR>Module R M₂<VAR>Module R M₃<VAR>Invertible 2<VAR>Q₁ : QuadraticForm R M₁<VAR>Q₂ : QuadraticForm R M₂<VAR>Q₃ : QuadraticForm R M₃<GOAL>(Q₁.tensorAssoc Q₂ Q₃).toLinearEquiv = TensorProduct.assoc R M₁ M₂ M₃
<VAR>R : Type uR<VAR>M₁ : Type uM₁<VAR>M₂ : Type uM₂<VAR>M₃ : Type uM₃<VAR>CommRing R<VAR>AddCommGroup M₁<VAR>AddCommGroup M₂<VAR>AddCommGroup M₃<VAR>Module R M₁<VAR>Module R M₂<VAR>Module R M₃<VAR>Invertible 2<VAR>Q₁ : QuadraticForm R M₁<VAR>Q₂ : QuadraticForm R M₂<VAR>Q₃ : QuadraticForm R M₃<VAR>x : (M₁ ⊗[R] M₂) ⊗[R] M₃<GOAL>(Q₁.tensorAssoc Q₂ Q₃) x = (TensorProduct.assoc R M₁ M₂ M₃) x
<VAR>R : Type uR<VAR>M₁ : Type uM₁<VAR>M₂ : Type uM₂<VAR>M₃ : Type uM₃<VAR>CommRing R<VAR>AddCommGroup M₁<VAR>AddCommGroup M₂<VAR>AddCommGroup M₃<VAR>Module R M₁<VAR>Module R M₂<VAR>Module R M₃<VAR>Invertible 2<VAR>Q₁ : QuadraticForm R M₁<VAR>Q₂ : QuadraticForm R M₂<VAR>Q₃ : QuadraticForm R M₃<VAR>x : M₁ ⊗[R] M₂ ⊗[R] M₃<GOAL>(Q₁.tensorAssoc Q₂ Q₃).symm x = (TensorProduct.assoc R M₁ M₂ M₃).symm x
<VAR>R : Type uR<VAR>M₁ : Type uM₁<VAR>CommRing R<VAR>AddCommGroup M₁<VAR>Module R M₁<VAR>Invertible 2<VAR>Q₁ : QuadraticForm R M₁<GOAL>QuadraticMap.comp Q₁ ↑(TensorProduct.rid R M₁) = Q₁.tmul QuadraticMap.sq
<VAR>R : Type uR<VAR>M₁ : Type uM₁<VAR>CommRing R<VAR>AddCommGroup M₁<VAR>Module R M₁<VAR>Invertible 2<VAR>Q₁ : QuadraticForm R M₁<VAR>x : M₁ ⊗[R] R<GOAL>Q₁ ((TensorProduct.rid R M₁) x) = (Q₁.tmul QuadraticMap.sq) x
<VAR>R : Type uR<VAR>M₁ : Type uM₁<VAR>CommRing R<VAR>AddCommGroup M₁<VAR>Module R M₁<VAR>Invertible 2<VAR>Q₁ : QuadraticForm R M₁<GOAL>Q₁.tensorRId.toLinearEquiv = TensorProduct.rid R M₁
<VAR>R : Type uR<VAR>M₁ : Type uM₁<VAR>CommRing R<VAR>AddCommGroup M₁<VAR>Module R M₁<VAR>Invertible 2<VAR>Q₁ : QuadraticForm R M₁<VAR>x : M₁ ⊗[R] R<GOAL>Q₁.tensorRId x = (TensorProduct.rid R M₁) x
<VAR>R : Type uR<VAR>M₁ : Type uM₁<VAR>CommRing R<VAR>AddCommGroup M₁<VAR>Module R M₁<VAR>Invertible 2<VAR>Q₁ : QuadraticForm R M₁<VAR>x : M₁<GOAL>Q₁.tensorRId.symm x = (TensorProduct.rid R M₁).symm x
<VAR>R : Type uR<VAR>M₂ : Type uM₂<VAR>CommRing R<VAR>AddCommGroup M₂<VAR>Module R M₂<VAR>Invertible 2<VAR>Q₂ : QuadraticForm R M₂<GOAL>QuadraticMap.comp Q₂ ↑(TensorProduct.lid R M₂) = QuadraticForm.tmul QuadraticMap.sq Q₂
<VAR>R : Type uR<VAR>M₂ : Type uM₂<VAR>CommRing R<VAR>AddCommGroup M₂<VAR>Module R M₂<VAR>Invertible 2<VAR>Q₂ : QuadraticForm R M₂<VAR>x : R ⊗[R] M₂<GOAL>Q₂ ((TensorProduct.lid R M₂) x) = (QuadraticForm.tmul QuadraticMap.sq Q₂) x
<VAR>R : Type uR<VAR>M₂ : Type uM₂<VAR>CommRing R<VAR>AddCommGroup M₂<VAR>Module R M₂<VAR>Invertible 2<VAR>Q₂ : QuadraticForm R M₂<GOAL>Q₂.tensorLId.toLinearEquiv = TensorProduct.lid R M₂
<VAR>R : Type uR<VAR>M₂ : Type uM₂<VAR>CommRing R<VAR>AddCommGroup M₂<VAR>Module R M₂<VAR>Invertible 2<VAR>Q₂ : QuadraticForm R M₂<VAR>x : R ⊗[R] M₂<GOAL>Q₂.tensorLId x = (TensorProduct.lid R M₂) x
<VAR>R : Type uR<VAR>M₂ : Type uM₂<VAR>CommRing R<VAR>AddCommGroup M₂<VAR>Module R M₂<VAR>Invertible 2<VAR>Q₂ : QuadraticForm R M₂<VAR>x : M₂<GOAL>Q₂.tensorLId.symm x = (TensorProduct.lid R M₂).symm x
<VAR>R : Type u_1<VAR>S : Type u_3<VAR>M : Type u_2<VAR>CommRing R<VAR>Field S<VAR>AddCommGroup M<VAR>Algebra R S<VAR>Module R M<VAR>Module S M<VAR>IsScalarTower R S M<VAR>B : LinearMap.BilinForm S M<VAR>N : Submodule R M<VAR>x : M<GOAL>x ∈ B.dualSubmodule N ↔ ∀ y ∈ N, (B x) y ∈ 1
<VAR>R : Type u_1<VAR>S : Type u_3<VAR>M : Type u_2<VAR>CommRing R<VAR>Field S<VAR>AddCommGroup M<VAR>Algebra R S<VAR>Module R M<VAR>Module S M<VAR>IsScalarTower R S M<VAR>B : LinearMap.BilinForm S M<VAR>N₁ N₂ : Submodule R M<GOAL>N₁ ≤ B.flip.dualSubmodule N₂ ↔ N₂ ≤ B.dualSubmodule N₁
<VAR>R : Type u_1<VAR>S : Type u_3<VAR>M : Type u_2<VAR>CommRing R<VAR>Field S<VAR>AddCommGroup M<VAR>Algebra R S<VAR>Module R M<VAR>Module S M<VAR>IsScalarTower R S M<VAR>B : LinearMap.BilinForm S M<VAR>N : Submodule R M<VAR>x : ↥(B.dualSubmodule N)<VAR>y : ↥N<GOAL>(algebraMap R S) (B.dualSubmoduleParing x y) = (B ↑x) ↑y
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>M : Type u_3<VAR>CommRing R<VAR>Field S<VAR>AddCommGroup M<VAR>Algebra R S<VAR>Module R M<VAR>Module S M<VAR>IsScalarTower R S M<VAR>B : LinearMap.BilinForm S M<VAR>NoZeroSMulDivisors R S<VAR>N : Submodule R M<VAR>x : ↥(B.dualSubmodule N)<VAR>y : ↥N<GOAL>((B.dualSubmoduleToDual N) x) y = B.dualSubmoduleParing x y
<VAR>R : Type u_3<VAR>S : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>Field S<VAR>AddCommGroup M<VAR>Algebra R S<VAR>Module R M<VAR>Module S M<VAR>IsScalarTower R S M<VAR>B : LinearMap.BilinForm S M<VAR>hB : B.Nondegenerate<VAR>NoZeroSMulDivisors R S<VAR>N : Submodule R M<VAR>hN : Submodule.span S ↑N = ⊤<GOAL>Function.Injective ⇑(B.dualSubmoduleToDual N)
<VAR>R : Type u_4<VAR>S : Type u_2<VAR>M : Type u_3<VAR>CommRing R<VAR>Field S<VAR>AddCommGroup M<VAR>Algebra R S<VAR>Module R M<VAR>Module S M<VAR>IsScalarTower R S M<VAR>B : LinearMap.BilinForm S M<VAR>ι : Type u_1<VAR>Finite ι<VAR>DecidableEq ι<VAR>hB : B.Nondegenerate<VAR>b : Basis ι S M<GOAL>B.dualSubmodule (Submodule.span R (Set.range ⇑b)) = Submodule.span R (Set.range ⇑(B.dualBasis hB b))
<VAR>R : Type u_4<VAR>S : Type u_2<VAR>M : Type u_3<VAR>CommRing R<VAR>Field S<VAR>AddCommGroup M<VAR>Algebra R S<VAR>Module R M<VAR>Module S M<VAR>IsScalarTower R S M<VAR>B : LinearMap.BilinForm S M<VAR>ι : Type u_1<VAR>Finite ι<VAR>hB : B.Nondegenerate<VAR>b : Basis ι S M<GOAL>B.dualSubmodule (B.flip.dualSubmodule (Submodule.span R (Set.range ⇑b))) = Submodule.span R (Set.range ⇑b)
<VAR>R : Type u_4<VAR>S : Type u_2<VAR>M : Type u_3<VAR>CommRing R<VAR>Field S<VAR>AddCommGroup M<VAR>Algebra R S<VAR>Module R M<VAR>Module S M<VAR>IsScalarTower R S M<VAR>B : LinearMap.BilinForm S M<VAR>ι : Type u_1<VAR>Finite ι<VAR>hB : B.Nondegenerate<VAR>b : Basis ι S M<GOAL>B.flip.dualSubmodule (B.dualSubmodule (Submodule.span R (Set.range ⇑b))) = Submodule.span R (Set.range ⇑b)
<VAR>R : Type u_4<VAR>S : Type u_2<VAR>M : Type u_3<VAR>CommRing R<VAR>Field S<VAR>AddCommGroup M<VAR>Algebra R S<VAR>Module R M<VAR>Module S M<VAR>IsScalarTower R S M<VAR>B : LinearMap.BilinForm S M<VAR>ι : Type u_1<VAR>Finite ι<VAR>hB : B.Nondegenerate<VAR>hB' : B.IsSymm<VAR>b : Basis ι S M<GOAL>B.dualSubmodule (B.dualSubmodule (Submodule.span R (Set.range ⇑b))) = Submodule.span R (Set.range ⇑b)
<VAR>R : Type uR<VAR>A : Type uA<VAR>M₁ : Type uM₁<VAR>M₂ : Type uM₂<VAR>CommSemiring R<VAR>CommSemiring A<VAR>AddCommMonoid M₁<VAR>AddCommMonoid M₂<VAR>Algebra R A<VAR>Module R M₁<VAR>Module A M₁<VAR>SMulCommClass R A M₁<VAR>IsScalarTower R A M₁<VAR>Module R M₂<VAR>B₁ : LinearMap.BilinForm A M₁<VAR>B₂ : LinearMap.BilinForm R M₂<VAR>m₁ : M₁<VAR>m₂ : M₂<VAR>m₁' : M₁<VAR>m₂' : M₂<GOAL>(((LinearMap.BilinMap.tensorDistrib R A) (B₁ ⊗ₜ[R] B₂)) (m₁ ⊗ₜ[R] m₂)) (m₁' ⊗ₜ[R] m₂') = (B₂ m₂) m₂' • (B₁ m₁) m₁'
<VAR>R : Type uR<VAR>A : Type uA<VAR>M₁ : Type uM₁<VAR>M₂ : Type uM₂<VAR>CommSemiring R<VAR>CommSemiring A<VAR>AddCommMonoid M₁<VAR>AddCommMonoid M₂<VAR>Algebra R A<VAR>Module R M₁<VAR>Module A M₁<VAR>SMulCommClass R A M₁<VAR>IsScalarTower R A M₁<VAR>Module R M₂<VAR>B₁ : LinearMap.BilinMap A M₁ A<VAR>B₂ : LinearMap.BilinMap R M₂ R<VAR>hB₁ : LinearMap.IsSymm B₁<VAR>hB₂ : LinearMap.IsSymm B₂<GOAL>LinearMap.IsSymm (B₁.tmul B₂)
<VAR>R : Type uR<VAR>A : Type uA<VAR>M₂ : Type uM₂<VAR>CommSemiring R<VAR>CommSemiring A<VAR>AddCommMonoid M₂<VAR>Algebra R A<VAR>Module R M₂<VAR>B₂ : LinearMap.BilinMap R M₂ R<VAR>a : A<VAR>m₂ : M₂<VAR>a' : A<VAR>m₂' : M₂<GOAL>((LinearMap.BilinMap.baseChange A B₂) (a ⊗ₜ[R] m₂)) (a' ⊗ₜ[R] m₂') = (B₂ m₂) m₂' • (a * a')
<VAR>R : Type uR<VAR>A : Type uA<VAR>M₂ : Type uM₂<VAR>CommSemiring R<VAR>CommSemiring A<VAR>AddCommMonoid M₂<VAR>Algebra R A<VAR>Module R M₂<VAR>B₂ : LinearMap.BilinForm R M₂<VAR>hB₂ : LinearMap.IsSymm B₂<GOAL>LinearMap.IsSymm (LinearMap.BilinMap.baseChange A B₂)
<VAR>R : Type uR<VAR>M₁ : Type uM₁<VAR>M₂ : Type uM₂<VAR>CommRing R<VAR>AddCommGroup M₁<VAR>AddCommGroup M₂<VAR>Module R M₁<VAR>Module R M₂<VAR>Module.Free R M₁<VAR>Module.Finite R M₁<VAR>Module.Free R M₂<VAR>Module.Finite R M₂<VAR>B₁ : LinearMap.BilinForm R M₁<VAR>B₂ : LinearMap.BilinForm R M₂<VAR>m₁ : M₁<VAR>m₂ : M₂<VAR>m₁' : M₁<VAR>m₂' : M₂<GOAL>(((LinearMap.BilinMap.tensorDistribEquiv R) (B₁ ⊗ₜ[R] B₂)) (m₁ ⊗ₜ[R] m₂)) (m₁' ⊗ₜ[R] m₂') = (B₁ m₁) m₁' * (B₂ m₂) m₂'
<VAR>R : Type uR<VAR>M₁ : Type uM₁<VAR>M₂ : Type uM₂<VAR>CommRing R<VAR>AddCommGroup M₁<VAR>AddCommGroup M₂<VAR>Module R M₁<VAR>Module R M₂<VAR>Module.Free R M₁<VAR>Module.Finite R M₁<VAR>Module.Free R M₂<VAR>Module.Finite R M₂<GOAL>↑(LinearMap.BilinMap.tensorDistribEquiv R) = LinearMap.BilinMap.tensorDistrib R R
<VAR>R : Type uR<VAR>M₁ : Type uM₁<VAR>M₂ : Type uM₂<VAR>CommRing R<VAR>AddCommGroup M₁<VAR>AddCommGroup M₂<VAR>Module R M₁<VAR>Module R M₂<VAR>Module.Free R M₁<VAR>Module.Finite R M₁<VAR>Module.Free R M₂<VAR>Module.Finite R M₂<VAR>B : LinearMap.BilinForm R M₁ ⊗[R] LinearMap.BilinForm R M₂<GOAL>(LinearMap.BilinMap.tensorDistribEquiv R) B = (LinearMap.BilinMap.tensorDistrib R R) B
<VAR>R : Type u_1<VAR>CommRing R<VAR>n : ℕ<VAR>v : Fin n → R<VAR>i j : Fin n<GOAL>Matrix.vandermonde v i j = v i ^ ↑j
<VAR>R : Type u_1<VAR>CommRing R<VAR>n : ℕ<VAR>v0 : R<VAR>v : Fin n → R<GOAL>Matrix.vandermonde (Fin.cons v0 v) = Fin.cons (fun j => v0 ^ ↑j) fun i => Fin.cons 1 fun j => v i * Matrix.vandermonde v i j
<VAR>R : Type u_1<VAR>CommRing R<VAR>n : ℕ<VAR>v : Fin n.succ → R<GOAL>Matrix.vandermonde v = Fin.cons (fun j => v 0 ^ ↑j) fun i => Fin.cons 1 fun j => v i.succ * Matrix.vandermonde (Fin.tail v) i j
<VAR>R : Type u_1<VAR>CommRing R<VAR>n : ℕ<VAR>v w : Fin n → R<VAR>i j : Fin n<GOAL>(Matrix.vandermonde v * (Matrix.vandermonde w)ᵀ) i j = ∑ k : Fin n, (v i * w j) ^ ↑k
<VAR>R : Type u_1<VAR>CommRing R<VAR>n : ℕ<VAR>v : Fin n → R<VAR>i j : Fin n<GOAL>((Matrix.vandermonde v)ᵀ * Matrix.vandermonde v) i j = ∑ k : Fin n, v k ^ (↑i + ↑j)
<VAR>R : Type u_1<VAR>CommRing R<VAR>n : ℕ<VAR>v : Fin n → R<GOAL>(Matrix.vandermonde v).det = ∏ i : Fin n, ∏ j ∈ Finset.Ioi i, (v j - v i)
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDomain R<VAR>n : ℕ<VAR>v : Fin n → R<GOAL>(Matrix.vandermonde v).det = 0 ↔ ∃ i j, v i = v j ∧ i ≠ j
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDomain R<VAR>n : ℕ<VAR>v : Fin n → R<GOAL>(Matrix.vandermonde v).det ≠ 0 ↔ Function.Injective v
<VAR>R : Type u_1<VAR>CommRing R<VAR>n : ℕ<VAR>v : Fin n → R<VAR>a : R<GOAL>(Matrix.vandermonde fun i => v i + a).det = (Matrix.vandermonde v).det
<VAR>R : Type u_1<VAR>CommRing R<VAR>n : ℕ<VAR>v : Fin n → R<VAR>a : R<GOAL>(Matrix.vandermonde fun i => v i - a).det = (Matrix.vandermonde v).det
<VAR>R : Type u_2<VAR>CommRing R<VAR>IsDomain R<VAR>n : ℕ<VAR>f v : Fin n → R<VAR>hf : Function.Injective f<VAR>hfv : ∀ (j : Fin n), ∑ i : Fin n, f j ^ ↑i * v i = 0<GOAL>v = 0
<VAR>R : Type u_2<VAR>CommRing R<VAR>IsDomain R<VAR>n : ℕ<VAR>f v : Fin n → R<VAR>hf : Function.Injective f<VAR>hfv : ∀ (j : Fin n), ∑ i : Fin n, v i * f j ^ ↑i = 0<GOAL>v = 0
<VAR>R : Type u_2<VAR>CommRing R<VAR>IsDomain R<VAR>n : ℕ<VAR>f v : Fin n → R<VAR>hf : Function.Injective f<VAR>hfv : ∀ (i : Fin n), ∑ j : Fin n, v j * f j ^ ↑i = 0<GOAL>v = 0
<VAR>R : Type u_1<VAR>CommRing R<VAR>n : ℕ<VAR>v : Fin n → R<VAR>p : Fin n → Polynomial R<VAR>h_deg : ∀ (i : Fin n), (p i).natDegree ≤ ↑i<GOAL>(Matrix.of fun i j => Polynomial.eval (v i) (p j)) = Matrix.vandermonde v * Matrix.of fun i j => (p j).coeff ↑i
<VAR>R : Type u_1<VAR>CommRing R<VAR>n : ℕ<VAR>v : Fin n → R<VAR>p : Fin n → Polynomial R<VAR>h_deg : ∀ (i : Fin n), (p i).natDegree = ↑i<VAR>h_monic : ∀ (i : Fin n), (p i).Monic<GOAL>(Matrix.vandermonde v).det = (Matrix.of fun i j => Polynomial.eval (v i) (p j)).det
<VAR>R : Type u_2<VAR>M₂ : Type u_3<VAR>CommRing R<VAR>AddCommGroup M₂<VAR>Module R M₂<VAR>Module.Finite R M₂<VAR>Module.Free R M₂<VAR>n : ℕ<VAR>N : Fin n → Type u_5<VAR>(i : Fin n) → AddCommGroup (N i)<VAR>(i : Fin n) → Module R (N i)<VAR>∀ (i : Fin n), Module.Finite R (N i)<VAR>∀ (i : Fin n), Module.Free R (N i)<GOAL>Module.Free R (MultilinearMap R N M₂) ∧ Module.Finite R (MultilinearMap R N M₂)
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M₂ : Type u_3<VAR>M₁ : ι → Type u_4<VAR>Finite ι<VAR>CommRing R<VAR>AddCommGroup M₂<VAR>Module R M₂<VAR>Module.Finite R M₂<VAR>Module.Free R M₂<VAR>(i : ι) → AddCommGroup (M₁ i)<VAR>(i : ι) → Module R (M₁ i)<VAR>∀ (i : ι), Module.Finite R (M₁ i)<VAR>∀ (i : ι), Module.Free R (M₁ i)<GOAL>Module.Free R (MultilinearMap R M₁ M₂) ∧ Module.Finite R (MultilinearMap R M₁ M₂)
<VAR>R : Type u_1<VAR>ι₁ : Type u_2<VAR>ι₂ : Type u_3<VAR>CommSemiring R<VAR>N₁ : Type u_6<VAR>AddCommMonoid N₁<VAR>Module R N₁<VAR>N₂ : Type u_7<VAR>AddCommMonoid N₂<VAR>Module R N₂<VAR>N : Type u_8<VAR>AddCommMonoid N<VAR>Module R N<VAR>a : MultilinearMap R (fun x => N) N₁<VAR>b : MultilinearMap R (fun x => N) N₂<VAR>v : ι₁ ⊕ ι₂ → N<GOAL>(a.domCoprod b) v = (a fun i => v (Sum.inl i)) ⊗ₜ[R] b fun i => v (Sum.inr i)
<VAR>R : Type u_1<VAR>ι₁ : Type u_2<VAR>ι₂ : Type u_3<VAR>CommSemiring R<VAR>N₁ : Type u_6<VAR>AddCommMonoid N₁<VAR>Module R N₁<VAR>N₂ : Type u_7<VAR>AddCommMonoid N₂<VAR>Module R N₂<VAR>N : Type u_8<VAR>AddCommMonoid N<VAR>Module R N<VAR>a : MultilinearMap R (fun x => N) N₁<VAR>b : MultilinearMap R (fun x => N) N₂<GOAL>MultilinearMap.domCoprod' (a ⊗ₜ[R] b) = a.domCoprod b