ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>CommSemiring 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_4<VAR>DecidableEq ι<VAR>p : ι →₀ M<VAR>n : N<VAR>i : ι<GOAL>((TensorProduct.finsuppLeft R M N ι) (p ⊗ₜ[R] n)) i = p i ⊗ₜ[R] n
<VAR>R : Type u_1<VAR>CommSemiring 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_4<VAR>DecidableEq ι<VAR>t : (ι →₀ M) ⊗[R] N<VAR>i : ι<GOAL>((TensorProduct.finsuppLeft R M N ι) t) i = (LinearMap.rTensor N (Finsupp.lapply i)) t
<VAR>R : Type u_1<VAR>CommSemiring 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_4<VAR>DecidableEq ι<VAR>i : ι<VAR>m : M<VAR>n : N<GOAL>(TensorProduct.finsuppLeft R M N ι).symm (Finsupp.single i (m ⊗ₜ[R] n)) = Finsupp.single i m ⊗ₜ[R] n
<VAR>R : Type u_1<VAR>CommSemiring 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_4<VAR>DecidableEq ι<VAR>m : M<VAR>p : ι →₀ N<GOAL>(TensorProduct.finsuppRight R M N ι) (m ⊗ₜ[R] p) = p.sum fun i n => Finsupp.single i (m ⊗ₜ[R] n)
<VAR>R : Type u_1<VAR>CommSemiring 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_4<VAR>DecidableEq ι<VAR>m : M<VAR>p : ι →₀ N<VAR>i : ι<GOAL>((TensorProduct.finsuppRight R M N ι) (m ⊗ₜ[R] p)) i = m ⊗ₜ[R] p i
<VAR>R : Type u_1<VAR>CommSemiring 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_4<VAR>DecidableEq ι<VAR>t : M ⊗[R] (ι →₀ N)<VAR>i : ι<GOAL>((TensorProduct.finsuppRight R M N ι) t) i = (LinearMap.lTensor M (Finsupp.lapply i)) t
<VAR>R : Type u_1<VAR>CommSemiring 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_4<VAR>DecidableEq ι<VAR>i : ι<VAR>m : M<VAR>n : N<GOAL>(TensorProduct.finsuppRight R M N ι).symm (Finsupp.single i (m ⊗ₜ[R] n)) = m ⊗ₜ[R] Finsupp.single i n
<VAR>R : Type u_1<VAR>CommSemiring 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_4<VAR>DecidableEq ι<VAR>S : Type u_5<VAR>CommSemiring S<VAR>Algebra R S<VAR>Module S M<VAR>IsScalarTower R S M<VAR>s : S<VAR>t : (ι →₀ M) ⊗[R] N<GOAL>(TensorProduct.finsuppLeft R M N ι) (s • t) = s • (TensorProduct.finsuppLeft R M N ι) t
<VAR>R : Type u_1<VAR>CommSemiring 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_4<VAR>DecidableEq ι<VAR>S : Type u_5<VAR>CommSemiring S<VAR>Algebra R S<VAR>Module S M<VAR>IsScalarTower R S M<VAR>x : (ι →₀ M) ⊗[R] N<GOAL>(TensorProduct.finsuppLeft' R M N ι S) x = (TensorProduct.finsuppLeft R M N ι) x
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>N : Type u_3<VAR>AddCommMonoid N<VAR>Module R N<VAR>ι : Type u_4<VAR>DecidableEq ι<VAR>p : ι →₀ R<VAR>n : N<VAR>i : ι<GOAL>((TensorProduct.finsuppScalarLeft R N ι) (p ⊗ₜ[R] n)) i = p i • n
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>N : Type u_3<VAR>AddCommMonoid N<VAR>Module R N<VAR>ι : Type u_4<VAR>DecidableEq ι<VAR>p : ι →₀ R<VAR>n : N<GOAL>(TensorProduct.finsuppScalarLeft R N ι) (p ⊗ₜ[R] n) = p.sum fun i m => Finsupp.single i (m • n)
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>N : Type u_3<VAR>AddCommMonoid N<VAR>Module R N<VAR>ι : Type u_4<VAR>DecidableEq ι<VAR>pn : (ι →₀ R) ⊗[R] N<VAR>i : ι<GOAL>((TensorProduct.finsuppScalarLeft R N ι) pn) i = (TensorProduct.lid R N) ((LinearMap.rTensor N (Finsupp.lapply i)) pn)
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>N : Type u_3<VAR>AddCommMonoid N<VAR>Module R N<VAR>ι : Type u_4<VAR>DecidableEq ι<VAR>i : ι<VAR>n : N<GOAL>(TensorProduct.finsuppScalarLeft R N ι).symm (Finsupp.single i n) = Finsupp.single i 1 ⊗ₜ[R] n
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_2<VAR>AddCommMonoid M<VAR>Module R M<VAR>ι : Type u_4<VAR>DecidableEq ι<VAR>m : M<VAR>p : ι →₀ R<VAR>i : ι<GOAL>((TensorProduct.finsuppScalarRight R M ι) (m ⊗ₜ[R] p)) i = p i • m
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_2<VAR>AddCommMonoid M<VAR>Module R M<VAR>ι : Type u_4<VAR>DecidableEq ι<VAR>m : M<VAR>p : ι →₀ R<GOAL>(TensorProduct.finsuppScalarRight R M ι) (m ⊗ₜ[R] p) = p.sum fun i n => Finsupp.single i (n • m)
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_2<VAR>AddCommMonoid M<VAR>Module R M<VAR>ι : Type u_4<VAR>DecidableEq ι<VAR>t : M ⊗[R] (ι →₀ R)<VAR>i : ι<GOAL>((TensorProduct.finsuppScalarRight R M ι) t) i = (TensorProduct.rid R M) ((LinearMap.lTensor M (Finsupp.lapply i)) t)
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_2<VAR>AddCommMonoid M<VAR>Module R M<VAR>ι : Type u_4<VAR>DecidableEq ι<VAR>i : ι<VAR>m : M<GOAL>(TensorProduct.finsuppScalarRight R M ι).symm (Finsupp.single i m) = m ⊗ₜ[R] Finsupp.single i 1
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>AddCommMonoid N<VAR>Module R N<VAR>Semiring S<VAR>Algebra R S<VAR>Module S M<VAR>IsScalarTower R S M<VAR>i : ι<VAR>m : M<VAR>k : κ<VAR>n : N<GOAL>(finsuppTensorFinsupp R S M N ι κ) (Finsupp.single i m ⊗ₜ[R] Finsupp.single k n) = Finsupp.single (i, k) (m ⊗ₜ[R] n)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>AddCommMonoid N<VAR>Module R N<VAR>Semiring S<VAR>Algebra R S<VAR>Module S M<VAR>IsScalarTower R S M<VAR>f : ι →₀ M<VAR>g : κ →₀ N<VAR>i : ι<VAR>k : κ<GOAL>((finsuppTensorFinsupp R S M N ι κ) (f ⊗ₜ[R] g)) (i, k) = f i ⊗ₜ[R] g k
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>AddCommMonoid N<VAR>Module R N<VAR>Semiring S<VAR>Algebra R S<VAR>Module S M<VAR>IsScalarTower R S M<VAR>i : ι × κ<VAR>m : M<VAR>n : N<GOAL>(finsuppTensorFinsupp R S M N ι κ).symm (Finsupp.single i (m ⊗ₜ[R] n)) = Finsupp.single i.1 m ⊗ₜ[R] Finsupp.single i.2 n
<VAR>R : Type u_1<VAR>N : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>CommSemiring R<VAR>AddCommMonoid N<VAR>Module R N<VAR>f : ι →₀ R<VAR>g : κ →₀ N<VAR>a : ι<VAR>b : κ<GOAL>((finsuppTensorFinsuppLid R N ι κ) (f ⊗ₜ[R] g)) (a, b) = f a • g b
<VAR>R : Type u_1<VAR>N : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>CommSemiring R<VAR>AddCommMonoid N<VAR>Module R N<VAR>a : ι<VAR>b : κ<VAR>r : R<VAR>n : N<GOAL>(finsuppTensorFinsuppLid R N ι κ) (Finsupp.single a r ⊗ₜ[R] Finsupp.single b n) = Finsupp.single (a, b) (r • n)
<VAR>R : Type u_1<VAR>N : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>CommSemiring R<VAR>AddCommMonoid N<VAR>Module R N<VAR>i : ι × κ<VAR>r : R<VAR>n : N<GOAL>(finsuppTensorFinsuppLid R N ι κ).symm (Finsupp.single i (r • n)) = Finsupp.single i.1 r ⊗ₜ[R] Finsupp.single i.2 n
<VAR>R : Type u_1<VAR>M : Type u_3<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>f : ι →₀ M<VAR>g : κ →₀ R<VAR>a : ι<VAR>b : κ<GOAL>((finsuppTensorFinsuppRid R M ι κ) (f ⊗ₜ[R] g)) (a, b) = g b • f a
<VAR>R : Type u_1<VAR>M : Type u_3<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>a : ι<VAR>b : κ<VAR>m : M<VAR>r : R<GOAL>(finsuppTensorFinsuppRid R M ι κ) (Finsupp.single a m ⊗ₜ[R] Finsupp.single b r) = Finsupp.single (a, b) (r • m)
<VAR>R : Type u_1<VAR>M : Type u_3<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>i : ι × κ<VAR>m : M<VAR>r : R<GOAL>(finsuppTensorFinsuppRid R M ι κ).symm (Finsupp.single i (r • m)) = Finsupp.single i.1 m ⊗ₜ[R] Finsupp.single i.2 r
<VAR>R : Type u_1<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>CommSemiring R<VAR>f : ι →₀ R<VAR>g : κ →₀ R<VAR>a : ι<VAR>b : κ<GOAL>((finsuppTensorFinsupp' R ι κ) (f ⊗ₜ[R] g)) (a, b) = f a * g b
<VAR>R : Type u_1<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>CommSemiring R<VAR>a : ι<VAR>b : κ<VAR>r₁ r₂ : R<GOAL>(finsuppTensorFinsupp' R ι κ) (Finsupp.single a r₁ ⊗ₜ[R] Finsupp.single b r₂) = Finsupp.single (a, b) (r₁ * r₂)
<VAR>R : Type u_1<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>CommSemiring R<VAR>i : ι × κ<VAR>r₁ r₂ : R<GOAL>(finsuppTensorFinsupp' R ι κ).symm (Finsupp.single i (r₁ * r₂)) = Finsupp.single i.1 r₁ ⊗ₜ[R] Finsupp.single i.2 r₂
<VAR>R : Type u_1<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>CommSemiring R<VAR>i : ι × κ<VAR>r : R<GOAL>(finsuppTensorFinsupp' R ι κ).symm (Finsupp.single i r) = Finsupp.single i.1 1 ⊗ₜ[R] Finsupp.single i.2 r
<VAR>R : Type u_1<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>CommSemiring R<VAR>i : ι × κ<VAR>r : R<GOAL>(finsuppTensorFinsupp' R ι κ).symm (Finsupp.single i r) = Finsupp.single i.1 r ⊗ₜ[R] Finsupp.single i.2 1
<VAR>R : Type u_1<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>CommSemiring R<GOAL>finsuppTensorFinsuppLid R R ι κ = finsuppTensorFinsupp' R ι κ
<VAR>R : Type u_1<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>CommSemiring R<GOAL>finsuppTensorFinsuppRid R R ι κ = finsuppTensorFinsupp' R ι κ
<VAR>ι : Type u_1<VAR>K : Type u_2<VAR>V : Type u_3<VAR>DivisionRing K<VAR>AddCommGroup V<VAR>Module K V<VAR>f : ι → ℙ K V<GOAL>Projectivization.Independent f ↔ LinearIndependent K (Projectivization.rep ∘ f)
<VAR>ι : Type u_1<VAR>K : Type u_2<VAR>V : Type u_3<VAR>DivisionRing K<VAR>AddCommGroup V<VAR>Module K V<VAR>f : ι → ℙ K V<GOAL>Projectivization.Independent f ↔ CompleteLattice.Independent fun i => (f i).submodule
<VAR>ι : Type u_1<VAR>K : Type u_2<VAR>V : Type u_3<VAR>DivisionRing K<VAR>AddCommGroup V<VAR>Module K V<VAR>f : ι → ℙ K V<GOAL>Projectivization.Dependent f ↔ ¬LinearIndependent K (Projectivization.rep ∘ f)
<VAR>ι : Type u_1<VAR>K : Type u_2<VAR>V : Type u_3<VAR>DivisionRing K<VAR>AddCommGroup V<VAR>Module K V<VAR>f : ι → ℙ K V<GOAL>Projectivization.Dependent f ↔ ¬Projectivization.Independent f
<VAR>ι : Type u_1<VAR>K : Type u_2<VAR>V : Type u_3<VAR>DivisionRing K<VAR>AddCommGroup V<VAR>Module K V<VAR>f : ι → ℙ K V<GOAL>Projectivization.Independent f ↔ ¬Projectivization.Dependent f
<VAR>K : Type u_2<VAR>V : Type u_3<VAR>DivisionRing K<VAR>AddCommGroup V<VAR>Module K V<VAR>u v : ℙ K V<GOAL>Projectivization.Dependent ![u, v] ↔ u = v
<VAR>K : Type u_2<VAR>V : Type u_3<VAR>DivisionRing K<VAR>AddCommGroup V<VAR>Module K V<VAR>u v : ℙ K V<GOAL>Projectivization.Independent ![u, v] ↔ u ≠ v
<VAR>R : Type u_1<VAR>n : Type u_2<VAR>M : Type u_3<VAR>DecidableEq n<VAR>Fintype n<VAR>CommRing R<VAR>Nontrivial R<VAR>AddCommGroup M<VAR>Module R M<VAR>d : n → R<VAR>i : n<VAR>b : Basis n R M<GOAL>Module.End.HasEigenvector ((Matrix.toLin b b) (Matrix.diagonal d)) (d i) (b i)
<VAR>R : Type u_1<VAR>n : Type u_2<VAR>DecidableEq n<VAR>Fintype n<VAR>CommRing R<VAR>Nontrivial R<VAR>d : n → R<VAR>i : n<GOAL>Module.End.HasEigenvector (Matrix.toLin' (Matrix.diagonal d)) (d i) ((Pi.basisFun R n) i)
<VAR>R : Type u_1<VAR>n : Type u_2<VAR>M : Type u_3<VAR>DecidableEq n<VAR>Fintype n<VAR>CommRing R<VAR>Nontrivial R<VAR>AddCommGroup M<VAR>Module R M<VAR>d : n → R<VAR>μ : R<VAR>NoZeroSMulDivisors R M<VAR>b : Basis n R M<GOAL>Module.End.HasEigenvalue ((Matrix.toLin b b) (Matrix.diagonal d)) μ ↔ ∃ i, d i = μ
<VAR>R : Type u_1<VAR>n : Type u_2<VAR>DecidableEq n<VAR>Fintype n<VAR>CommRing R<VAR>Nontrivial R<VAR>NoZeroDivisors R<VAR>d : n → R<VAR>μ : R<GOAL>Module.End.HasEigenvalue (Matrix.toLin' (Matrix.diagonal d)) μ ↔ ∃ i, d i = μ
<VAR>R : Type u_1<VAR>n : Type u_2<VAR>DecidableEq n<VAR>Fintype n<VAR>Field R<VAR>d : n → R<GOAL>spectrum R (Matrix.diagonal d) = Set.range d
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>CommSemiring ι<VAR>DecidableEq ι<VAR>CommRing R<VAR>Ring A<VAR>Ring B<VAR>Algebra R A<VAR>Algebra R B<VAR>𝒜 : ι → Submodule R A<VAR>ℬ : ι → Submodule R B<VAR>GradedAlgebra 𝒜<VAR>GradedAlgebra ℬ<GOAL>(GradedTensorProduct.of R 𝒜 ℬ) 1 = 1
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>CommSemiring ι<VAR>DecidableEq ι<VAR>CommRing R<VAR>Ring A<VAR>Ring B<VAR>Algebra R A<VAR>Algebra R B<VAR>𝒜 : ι → Submodule R A<VAR>ℬ : ι → Submodule R B<VAR>GradedAlgebra 𝒜<VAR>GradedAlgebra ℬ<GOAL>(GradedTensorProduct.of R 𝒜 ℬ).symm 1 = 1
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>CommSemiring ι<VAR>DecidableEq ι<VAR>CommRing R<VAR>Ring A<VAR>Ring B<VAR>Algebra R A<VAR>Algebra R B<VAR>𝒜 : ι → Submodule R A<VAR>ℬ : ι → Submodule R B<VAR>GradedAlgebra 𝒜<VAR>GradedAlgebra ℬ<VAR>x : A ⊗[R] B<GOAL>(GradedTensorProduct.of R 𝒜 ℬ).symm ((GradedTensorProduct.of R 𝒜 ℬ) x) = x
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>CommSemiring ι<VAR>DecidableEq ι<VAR>CommRing R<VAR>Ring A<VAR>Ring B<VAR>Algebra R A<VAR>Algebra R B<VAR>𝒜 : ι → Submodule R A<VAR>ℬ : ι → Submodule R B<VAR>GradedAlgebra 𝒜<VAR>GradedAlgebra ℬ<VAR>x : 𝒜 ᵍ⊗[R] ℬ<GOAL>(GradedTensorProduct.of R 𝒜 ℬ) ((GradedTensorProduct.of R 𝒜 ℬ).symm x) = x
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>CommSemiring ι<VAR>DecidableEq ι<VAR>CommRing R<VAR>Ring A<VAR>Ring B<VAR>Algebra R A<VAR>Algebra R B<VAR>𝒜 : ι → Submodule R A<VAR>ℬ : ι → Submodule R B<VAR>GradedAlgebra 𝒜<VAR>GradedAlgebra ℬ<VAR>M : Type u_5<VAR>AddCommMonoid M<VAR>Module R M<VAR>f g : 𝒜 ᵍ⊗[R] ℬ →ₗ[R] M<VAR>h : f ∘ₗ ↑(GradedTensorProduct.of R 𝒜 ℬ) = g ∘ₗ ↑(GradedTensorProduct.of R 𝒜 ℬ)<GOAL>f = g
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>CommSemiring ι<VAR>DecidableEq ι<VAR>CommRing R<VAR>Ring A<VAR>Ring B<VAR>Algebra R A<VAR>Algebra R B<VAR>𝒜 : ι → Submodule R A<VAR>ℬ : ι → Submodule R B<VAR>GradedAlgebra 𝒜<VAR>GradedAlgebra ℬ<VAR>a : A<VAR>b : B<GOAL>(GradedTensorProduct.auxEquiv R 𝒜 ℬ) (a ᵍ⊗ₜ[R] b) = (DirectSum.decompose 𝒜) a ⊗ₜ[R] (DirectSum.decompose ℬ) b
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>CommSemiring ι<VAR>DecidableEq ι<VAR>CommRing R<VAR>Ring A<VAR>Ring B<VAR>Algebra R A<VAR>Algebra R B<VAR>𝒜 : ι → Submodule R A<VAR>ℬ : ι → Submodule R B<VAR>GradedAlgebra 𝒜<VAR>GradedAlgebra ℬ<GOAL>(GradedTensorProduct.auxEquiv R 𝒜 ℬ) 1 = 1
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>CommSemiring ι<VAR>DecidableEq ι<VAR>CommRing R<VAR>Ring A<VAR>Ring B<VAR>Algebra R A<VAR>Algebra R B<VAR>𝒜 : ι → Submodule R A<VAR>ℬ : ι → Submodule R B<VAR>GradedAlgebra 𝒜<VAR>GradedAlgebra ℬ<GOAL>(GradedTensorProduct.auxEquiv R 𝒜 ℬ).symm 1 = 1
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>CommSemiring ι<VAR>Module ι (Additive ℤˣ)<VAR>DecidableEq ι<VAR>CommRing R<VAR>Ring A<VAR>Ring B<VAR>Algebra R A<VAR>Algebra R B<VAR>𝒜 : ι → Submodule R A<VAR>ℬ : ι → Submodule R B<VAR>GradedAlgebra 𝒜<VAR>GradedAlgebra ℬ<VAR>x y : 𝒜 ᵍ⊗[R] ℬ<GOAL>((GradedTensorProduct.mulHom 𝒜 ℬ) x) y = (GradedTensorProduct.auxEquiv R 𝒜 ℬ).symm (((TensorProduct.gradedMul R (fun x => ↥(𝒜 x)) fun x => ↥(ℬ x)) ((GradedTensorProduct.auxEquiv R 𝒜 ℬ) x)) ((GradedTensorProduct.auxEquiv R 𝒜 ℬ) y))
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>CommSemiring ι<VAR>Module ι (Additive ℤˣ)<VAR>DecidableEq ι<VAR>CommRing R<VAR>Ring A<VAR>Ring B<VAR>Algebra R A<VAR>Algebra R B<VAR>𝒜 : ι → Submodule R A<VAR>ℬ : ι → Submodule R B<VAR>GradedAlgebra 𝒜<VAR>GradedAlgebra ℬ<VAR>x y : 𝒜 ᵍ⊗[R] ℬ<GOAL>x * y = ((GradedTensorProduct.mulHom 𝒜 ℬ) x) y
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>CommSemiring ι<VAR>Module ι (Additive ℤˣ)<VAR>DecidableEq ι<VAR>CommRing R<VAR>Ring A<VAR>Ring B<VAR>Algebra R A<VAR>Algebra R B<VAR>𝒜 : ι → Submodule R A<VAR>ℬ : ι → Submodule R B<VAR>GradedAlgebra 𝒜<VAR>GradedAlgebra ℬ<VAR>x y : 𝒜 ᵍ⊗[R] ℬ<GOAL>(GradedTensorProduct.auxEquiv R 𝒜 ℬ) (x * y) = ((TensorProduct.gradedMul R (fun x => ↥(𝒜 x)) fun x => ↥(ℬ x)) ((GradedTensorProduct.auxEquiv R 𝒜 ℬ) x)) ((GradedTensorProduct.auxEquiv R 𝒜 ℬ) y)
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>CommSemiring ι<VAR>Module ι (Additive ℤˣ)<VAR>DecidableEq ι<VAR>CommRing R<VAR>Ring A<VAR>Ring B<VAR>Algebra R A<VAR>Algebra R B<VAR>𝒜 : ι → Submodule R A<VAR>ℬ : ι → Submodule R B<VAR>GradedAlgebra 𝒜<VAR>GradedAlgebra ℬ<VAR>j₁ i₂ : ι<VAR>a₁ : A<VAR>b₁ : ↥(ℬ j₁)<VAR>a₂ : ↥(𝒜 i₂)<VAR>b₂ : B<GOAL>a₁ ᵍ⊗ₜ[R] ↑b₁ * ↑a₂ ᵍ⊗ₜ[R] b₂ = (-1) ^ (j₁ * i₂) • (a₁ * ↑a₂) ᵍ⊗ₜ[R] (↑b₁ * b₂)
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>CommSemiring ι<VAR>Module ι (Additive ℤˣ)<VAR>DecidableEq ι<VAR>CommRing R<VAR>Ring A<VAR>Ring B<VAR>Algebra R A<VAR>Algebra R B<VAR>𝒜 : ι → Submodule R A<VAR>ℬ : ι → Submodule R B<VAR>GradedAlgebra 𝒜<VAR>GradedAlgebra ℬ<VAR>i₂ : ι<VAR>a₁ : A<VAR>b₁ : ↥(ℬ 0)<VAR>a₂ : ↥(𝒜 i₂)<VAR>b₂ : B<GOAL>a₁ ᵍ⊗ₜ[R] ↑b₁ * ↑a₂ ᵍ⊗ₜ[R] b₂ = (a₁ * ↑a₂) ᵍ⊗ₜ[R] (↑b₁ * b₂)
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>CommSemiring ι<VAR>Module ι (Additive ℤˣ)<VAR>DecidableEq ι<VAR>CommRing R<VAR>Ring A<VAR>Ring B<VAR>Algebra R A<VAR>Algebra R B<VAR>𝒜 : ι → Submodule R A<VAR>ℬ : ι → Submodule R B<VAR>GradedAlgebra 𝒜<VAR>GradedAlgebra ℬ<VAR>j₁ : ι<VAR>a₁ : A<VAR>b₁ : ↥(ℬ j₁)<VAR>a₂ : ↥(𝒜 0)<VAR>b₂ : B<GOAL>a₁ ᵍ⊗ₜ[R] ↑b₁ * ↑a₂ ᵍ⊗ₜ[R] b₂ = (a₁ * ↑a₂) ᵍ⊗ₜ[R] (↑b₁ * b₂)
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>CommSemiring ι<VAR>Module ι (Additive ℤˣ)<VAR>DecidableEq ι<VAR>CommRing R<VAR>Ring A<VAR>Ring B<VAR>Algebra R A<VAR>Algebra R B<VAR>𝒜 : ι → Submodule R A<VAR>ℬ : ι → Submodule R B<VAR>GradedAlgebra 𝒜<VAR>GradedAlgebra ℬ<VAR>i₂ : ι<VAR>a₁ : A<VAR>a₂ : ↥(𝒜 i₂)<VAR>b₂ : B<GOAL>a₁ ᵍ⊗ₜ[R] 1 * ↑a₂ ᵍ⊗ₜ[R] b₂ = (a₁ * ↑a₂) ᵍ⊗ₜ[R] b₂
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>CommSemiring ι<VAR>Module ι (Additive ℤˣ)<VAR>DecidableEq ι<VAR>CommRing R<VAR>Ring A<VAR>Ring B<VAR>Algebra R A<VAR>Algebra R B<VAR>𝒜 : ι → Submodule R A<VAR>ℬ : ι → Submodule R B<VAR>GradedAlgebra 𝒜<VAR>GradedAlgebra ℬ<VAR>j₁ : ι<VAR>a₁ : A<VAR>b₁ : ↥(ℬ j₁)<VAR>b₂ : B<GOAL>a₁ ᵍ⊗ₜ[R] ↑b₁ * 1 ᵍ⊗ₜ[R] b₂ = a₁ ᵍ⊗ₜ[R] (↑b₁ * b₂)
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>CommSemiring ι<VAR>Module ι (Additive ℤˣ)<VAR>DecidableEq ι<VAR>CommRing R<VAR>Ring A<VAR>Ring B<VAR>Algebra R A<VAR>Algebra R B<VAR>𝒜 : ι → Submodule R A<VAR>ℬ : ι → Submodule R B<VAR>GradedAlgebra 𝒜<VAR>GradedAlgebra ℬ<VAR>a₁ : A<VAR>b₂ : B<GOAL>a₁ ᵍ⊗ₜ[R] 1 * 1 ᵍ⊗ₜ[R] b₂ = a₁ ᵍ⊗ₜ[R] b₂
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>CommSemiring ι<VAR>Module ι (Additive ℤˣ)<VAR>DecidableEq ι<VAR>CommRing R<VAR>Ring A<VAR>Ring B<VAR>Algebra R A<VAR>Algebra R B<VAR>𝒜 : ι → Submodule R A<VAR>ℬ : ι → Submodule R B<VAR>GradedAlgebra 𝒜<VAR>GradedAlgebra ℬ<VAR>a : A<GOAL>(GradedTensorProduct.includeLeftRingHom 𝒜 ℬ) a = a ᵍ⊗ₜ[R] 1
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>CommSemiring ι<VAR>Module ι (Additive ℤˣ)<VAR>DecidableEq ι<VAR>CommRing R<VAR>Ring A<VAR>Ring B<VAR>Algebra R A<VAR>Algebra R B<VAR>𝒜 : ι → Submodule R A<VAR>ℬ : ι → Submodule R B<VAR>GradedAlgebra 𝒜<VAR>GradedAlgebra ℬ<VAR>r : R<GOAL>(algebraMap R (𝒜 ᵍ⊗[R] ℬ)) r = (algebraMap R A) r ᵍ⊗ₜ[R] 1
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>CommSemiring ι<VAR>Module ι (Additive ℤˣ)<VAR>DecidableEq ι<VAR>CommRing R<VAR>Ring A<VAR>Ring B<VAR>Algebra R A<VAR>Algebra R B<VAR>𝒜 : ι → Submodule R A<VAR>ℬ : ι → Submodule R B<VAR>GradedAlgebra 𝒜<VAR>GradedAlgebra ℬ<VAR>i₂ : ι<VAR>a₁ : A<VAR>r : R<VAR>a₂ : ↥(𝒜 i₂)<VAR>b₂ : B<GOAL>a₁ ᵍ⊗ₜ[R] (algebraMap R B) r * ↑a₂ ᵍ⊗ₜ[R] b₂ = (a₁ * ↑a₂) ᵍ⊗ₜ[R] ((algebraMap R B) r * b₂)
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>CommSemiring ι<VAR>Module ι (Additive ℤˣ)<VAR>DecidableEq ι<VAR>CommRing R<VAR>Ring A<VAR>Ring B<VAR>Algebra R A<VAR>Algebra R B<VAR>𝒜 : ι → Submodule R A<VAR>ℬ : ι → Submodule R B<VAR>GradedAlgebra 𝒜<VAR>GradedAlgebra ℬ<VAR>j₁ : ι<VAR>a₁ : A<VAR>b₁ : ↥(ℬ j₁)<VAR>r : R<VAR>b₂ : B<GOAL>a₁ ᵍ⊗ₜ[R] ↑b₁ * (algebraMap R A) r ᵍ⊗ₜ[R] b₂ = (a₁ * (algebraMap R A) r) ᵍ⊗ₜ[R] (↑b₁ * b₂)
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>CommSemiring ι<VAR>Module ι (Additive ℤˣ)<VAR>DecidableEq ι<VAR>CommRing R<VAR>Ring A<VAR>Ring B<VAR>Algebra R A<VAR>Algebra R B<VAR>𝒜 : ι → Submodule R A<VAR>ℬ : ι → Submodule R B<VAR>GradedAlgebra 𝒜<VAR>GradedAlgebra ℬ<VAR>a : A<GOAL>(GradedTensorProduct.includeLeft 𝒜 ℬ) a = a ᵍ⊗ₜ[R] 1
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>CommSemiring ι<VAR>Module ι (Additive ℤˣ)<VAR>DecidableEq ι<VAR>CommRing R<VAR>Ring A<VAR>Ring B<VAR>Algebra R A<VAR>Algebra R B<VAR>𝒜 : ι → Submodule R A<VAR>ℬ : ι → Submodule R B<VAR>GradedAlgebra 𝒜<VAR>GradedAlgebra ℬ<VAR>a : B<GOAL>(GradedTensorProduct.includeRight 𝒜 ℬ) a = 1 ᵍ⊗ₜ[R] a
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>CommSemiring ι<VAR>Module ι (Additive ℤˣ)<VAR>DecidableEq ι<VAR>CommRing R<VAR>Ring A<VAR>Ring B<VAR>Algebra R A<VAR>Algebra R B<VAR>𝒜 : ι → Submodule R A<VAR>ℬ : ι → Submodule R B<VAR>GradedAlgebra 𝒜<VAR>GradedAlgebra ℬ<VAR>r : R<GOAL>(algebraMap R (𝒜 ᵍ⊗[R] ℬ)) r = 1 ᵍ⊗ₜ[R] (algebraMap R B) r
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>CommSemiring ι<VAR>Module ι (Additive ℤˣ)<VAR>DecidableEq ι<VAR>CommRing R<VAR>Ring A<VAR>Ring B<VAR>Algebra R A<VAR>Algebra R B<VAR>𝒜 : ι → Submodule R A<VAR>ℬ : ι → Submodule R B<VAR>GradedAlgebra 𝒜<VAR>GradedAlgebra ℬ<VAR>C : Type u_5<VAR>Ring C<VAR>Algebra R C<VAR>f : A →ₐ[R] C<VAR>g : B →ₐ[R] C<VAR>h_anti_commutes : ∀ ⦃i j : ι⦄ (a : ↥(𝒜 i)) (b : ↥(ℬ j)), f ↑a * g ↑b = (-1) ^ (j * i) • (g ↑b * f ↑a)<VAR>a : A<VAR>b : B<GOAL>(GradedTensorProduct.lift 𝒜 ℬ f g h_anti_commutes) (a ᵍ⊗ₜ[R] b) = f a * g b
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>CommSemiring ι<VAR>Module ι (Additive ℤˣ)<VAR>DecidableEq ι<VAR>CommRing R<VAR>Ring A<VAR>Ring B<VAR>Algebra R A<VAR>Algebra R B<VAR>𝒜 : ι → Submodule R A<VAR>ℬ : ι → Submodule R B<VAR>GradedAlgebra 𝒜<VAR>GradedAlgebra ℬ<VAR>C : Type u_5<VAR>Ring C<VAR>Algebra R C<VAR>f g : 𝒜 ᵍ⊗[R] ℬ →ₐ[R] C<VAR>ha : f.comp (GradedTensorProduct.includeLeft 𝒜 ℬ) = g.comp (GradedTensorProduct.includeLeft 𝒜 ℬ)<VAR>hb : f.comp (GradedTensorProduct.includeRight 𝒜 ℬ) = g.comp (GradedTensorProduct.includeRight 𝒜 ℬ)<GOAL>f = g
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>CommSemiring ι<VAR>Module ι (Additive ℤˣ)<VAR>DecidableEq ι<VAR>CommRing R<VAR>Ring A<VAR>Ring B<VAR>Algebra R A<VAR>Algebra R B<VAR>𝒜 : ι → Submodule R A<VAR>ℬ : ι → Submodule R B<VAR>GradedAlgebra 𝒜<VAR>GradedAlgebra ℬ<VAR>x : 𝒜 ᵍ⊗[R] ℬ<GOAL>(GradedTensorProduct.auxEquiv R ℬ 𝒜) ((GradedTensorProduct.comm 𝒜 ℬ) x) = (TensorProduct.gradedComm R (fun x => ↥(𝒜 x)) fun x => ↥(ℬ x)) ((GradedTensorProduct.auxEquiv R 𝒜 ℬ) x)
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>CommSemiring ι<VAR>Module ι (Additive ℤˣ)<VAR>DecidableEq ι<VAR>CommRing R<VAR>Ring A<VAR>Ring B<VAR>Algebra R A<VAR>Algebra R B<VAR>𝒜 : ι → Submodule R A<VAR>ℬ : ι → Submodule R B<VAR>GradedAlgebra 𝒜<VAR>GradedAlgebra ℬ<VAR>i j : ι<VAR>a : ↥(𝒜 i)<VAR>b : ↥(ℬ j)<GOAL>(GradedTensorProduct.comm 𝒜 ℬ) (↑a ᵍ⊗ₜ[R] ↑b) = (-1) ^ (j * i) • ↑b ᵍ⊗ₜ[R] ↑a
<VAR>K : Type u_1<VAR>V : Type u_2<VAR>Field K<VAR>AddCommGroup V<VAR>Module K V<VAR>self : Projectivization.Subspace K V<VAR>v w : V<VAR>hv : v ≠ 0<VAR>hw : w ≠ 0<VAR>hvw : v + w ≠ 0<GOAL>Projectivization.mk K v hv ∈ self.carrier → Projectivization.mk K w hw ∈ self.carrier → Projectivization.mk K (v + w) hvw ∈ self.carrier
<VAR>K : Type u_1<VAR>V : Type u_2<VAR>Field K<VAR>AddCommGroup V<VAR>Module K V<VAR>A : Projectivization.Subspace K V<VAR>x : Projectivization K V<GOAL>x ∈ A.carrier ↔ x ∈ A
<VAR>K : Type u_1<VAR>V : Type u_2<VAR>Field K<VAR>AddCommGroup V<VAR>Module K V<VAR>T : Projectivization.Subspace K V<VAR>v w : V<VAR>hv : v ≠ 0<VAR>hw : w ≠ 0<VAR>hvw : v + w ≠ 0<GOAL>Projectivization.mk K v hv ∈ T → Projectivization.mk K w hw ∈ T → Projectivization.mk K (v + w) hvw ∈ T
<VAR>K : Type u_1<VAR>V : Type u_2<VAR>Field K<VAR>AddCommGroup V<VAR>Module K V<VAR>S : Set (Projectivization K V)<GOAL>S ⊆ ↑(Projectivization.Subspace.span S)
<VAR>K : Type u_1<VAR>V : Type u_2<VAR>Field K<VAR>AddCommGroup V<VAR>Module K V<VAR>W : Projectivization.Subspace K V<GOAL>Projectivization.Subspace.span ↑W = W
<VAR>K : Type u_1<VAR>V : Type u_2<VAR>Field K<VAR>AddCommGroup V<VAR>Module K V<GOAL>Projectivization.Subspace.span ∅ = ⊥
<VAR>K : Type u_1<VAR>V : Type u_2<VAR>Field K<VAR>AddCommGroup V<VAR>Module K V<GOAL>Projectivization.Subspace.span Set.univ = ⊤