ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u<VAR>M : Type v<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>ι : Type w<VAR>ι' : Type w'<VAR>StrongRankCondition R<VAR>N O : Submodule R M<VAR>hNO : N ≤ O<VAR>Fintype ι<VAR>b : Basis ι R ↥O<VAR>Fintype ι'<VAR>b' : Basis ι' R ↥N<GOAL>Fintype.card ι' ≤ Fintype.card ι
<VAR>R : Type u<VAR>M : Type v<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>ι : Type w<VAR>StrongRankCondition R<VAR>v : Basis ι R M<GOAL>Cardinal.lift.{v, w} #ι = Cardinal.lift.{w, v} (Module.rank R M)
<VAR>R : Type u<VAR>M : Type v<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>ι : Type w<VAR>StrongRankCondition R<VAR>v : Basis ι R M<GOAL>Cardinal.lift.{max v m, w} #ι = Cardinal.lift.{max w m, v} (Module.rank R M)
<VAR>R : Type u<VAR>M : Type v<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>ι : Type w<VAR>StrongRankCondition R<VAR>v : ι → M<VAR>hv : LinearIndependent R v<GOAL>Module.rank R ↥(Submodule.span R (Set.range v)) = #↑(Set.range v)
<VAR>R : Type u<VAR>M : Type v<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>StrongRankCondition R<VAR>s : Set M<VAR>hs : LinearIndependent R fun (x : ↑s) => ↑x<GOAL>Module.rank R ↥(Submodule.span R s) = #↑s
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>CommRing R<VAR>StrongRankCondition R<VAR>Ring S<VAR>IsDomain S<VAR>Algebra R S<VAR>n : Type u_3<VAR>m : Type u_4<VAR>Fintype n<VAR>Fintype m<VAR>b : Basis n R S<VAR>I : Ideal S<VAR>hI : I ≠ ⊥<VAR>c : Basis m R ↥I<GOAL>Fintype.card m = Fintype.card n
<VAR>R : Type u<VAR>M : Type v<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>ι : Type w<VAR>StrongRankCondition R<VAR>h : Basis ι R M<GOAL>FiniteDimensional.finrank R M = Nat.card ι
<VAR>R : Type u<VAR>M : Type v<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>StrongRankCondition R<VAR>ι : Type w<VAR>Fintype ι<VAR>h : Basis ι R M<GOAL>FiniteDimensional.finrank R M = Fintype.card ι
<VAR>R : Type u<VAR>M : Type v<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>StrongRankCondition R<VAR>Module.Finite R M<VAR>ι : Type w<VAR>h : Basis ι R M<GOAL>↑(FiniteDimensional.finrank R M) = #ι
<VAR>R : Type u<VAR>M : Type v<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>StrongRankCondition R<VAR>ι : Type w<VAR>b : Finset ι<VAR>h : Basis { x // x ∈ b } R M<GOAL>FiniteDimensional.finrank R M = b.card
<VAR>R : Type u<VAR>Ring R<VAR>StrongRankCondition R<GOAL>Module.rank R R = 1
<VAR>R : Type u<VAR>Ring R<VAR>StrongRankCondition R<GOAL>FiniteDimensional.finrank R R = 1
<VAR>R : Type u<VAR>M : Type v<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>StrongRankCondition R<VAR>Module.Finite R M<GOAL>Module.rank R M < ℵ₀
<VAR>R : Type u<VAR>M : Type v<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>StrongRankCondition R<VAR>Module.Finite R M<GOAL>↑(FiniteDimensional.finrank R M) = Module.rank R M
<VAR>R : Type u<VAR>M : Type v<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>StrongRankCondition R<VAR>M' : Type u_1<VAR>AddCommGroup M'<VAR>Module R M'<VAR>Module.Finite R M'<VAR>f : M →ₗ[R] M'<VAR>hf : Function.Injective ⇑f<GOAL>FiniteDimensional.finrank R M ≤ FiniteDimensional.finrank R M'
<VAR>R : Type u<VAR>M : Type v<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>StrongRankCondition R<VAR>M' : Type u_1<VAR>AddCommGroup M'<VAR>Module R M'<VAR>Module.Finite R M<VAR>f : M →ₗ[R] M'<GOAL>FiniteDimensional.finrank R ↥(LinearMap.range f) ≤ FiniteDimensional.finrank R M
<VAR>R : Type u_1<VAR>Semiring R<VAR>ι : Type u_2<VAR>DecidableEq ι<VAR>M : ι → Type u_3<VAR>(i : ι) → AddCommMonoid (M i)<VAR>(i : ι) → Module R (M i)<VAR>C : (⨁ (i : ι), M i) → Prop<VAR>x : ⨁ (i : ι), M i<VAR>H_zero : C 0<VAR>H_basic : ∀ (i : ι) (x : M i), C ((DirectSum.lof R ι M i) x)<VAR>H_plus : ∀ (x y : ⨁ (i : ι), M i), C x → C y → C (x + y)<GOAL>C x
<VAR>I : Type u<VAR>DecidableEq I<VAR>R : Type v<VAR>CommSemiring R<VAR>A : I → Type w<VAR>(i : I) → Semiring (A i)<VAR>(i : I) → Algebra R (A i)<VAR>i : I<GOAL>LinearAlgebra.FreeProduct.rel R A ((TensorAlgebra.ι R) ((DirectSum.lof R I A i) 1)) 1
<VAR>I : Type u<VAR>DecidableEq I<VAR>R : Type v<VAR>CommSemiring R<VAR>A : I → Type w<VAR>(i : I) → Semiring (A i)<VAR>(i : I) → Algebra R (A i)<VAR>x : ⨁ (i : I), A i<GOAL>{ toQuot := Quot.mk (RingQuot.Rel (LinearAlgebra.FreeProduct.rel R A)) ((TensorAlgebra.ι R) x) } = (LinearAlgebra.FreeProduct.ι' R A) x
<VAR>I : Type u<VAR>DecidableEq I<VAR>R : Type v<VAR>CommSemiring R<VAR>A : I → Type w<VAR>(i : I) → Semiring (A i)<VAR>(i : I) → Algebra R (A i)<VAR>i : I<GOAL>(LinearAlgebra.FreeProduct.ι' R A) ((DirectSum.lof R I A i) 1) = 1
<VAR>I : Type u<VAR>DecidableEq I<VAR>i : I<VAR>R : Type v<VAR>CommSemiring R<VAR>A : I → Type w<VAR>(i : I) → Semiring (A i)<VAR>(i : I) → Algebra R (A i)<VAR>a₁ a₂ : A i<GOAL>(LinearAlgebra.FreeProduct.ι' R A) ((DirectSum.lof R I A i) a₁) * (LinearAlgebra.FreeProduct.ι' R A) ((DirectSum.lof R I A i) a₂) = (LinearAlgebra.FreeProduct.ι' R A) ((DirectSum.lof R I A i) (a₁ * a₂))
<VAR>I : Type u<VAR>DecidableEq I<VAR>R : Type v<VAR>CommSemiring R<VAR>A : I → Type w<VAR>(i : I) → Semiring (A i)<VAR>(i : I) → Algebra R (A i)<VAR>i : I<GOAL>(LinearAlgebra.FreeProduct.lof R A i) 1 = 1
<VAR>I : Type u_1<VAR>DecidableEq I<VAR>R : Type u_2<VAR>CommSemiring R<VAR>A : I → Type u_3<VAR>(i : I) → Semiring (A i)<VAR>(i : I) → Algebra R (A i)<VAR>i : I<GOAL>LinearAlgebra.FreeProduct.ι R A i = AlgHom.ofLinearMap (LinearAlgebra.FreeProduct.ι' R A ∘ₗ DirectSum.lof R I A i) ⋯ ⋯
<VAR>I : Type u_1<VAR>DecidableEq I<VAR>R : Type u_2<VAR>CommSemiring R<VAR>A : I → Type u_3<VAR>(i : I) → Semiring (A i)<VAR>(i : I) → Algebra R (A i)<VAR>i : I<GOAL>LinearAlgebra.FreeProduct.of R A = LinearAlgebra.FreeProduct.ι R A i
<VAR>I : Type u<VAR>DecidableEq I<VAR>R : Type v<VAR>CommSemiring R<VAR>A : I → Type w<VAR>(i : I) → Semiring (A i)<VAR>(i : I) → Algebra R (A i)<VAR>B : Type w'<VAR>Semiring B<VAR>Algebra R B<VAR>π : LinearAlgebra.FreeProduct R A →ₐ[R] B<VAR>i : I<GOAL>(LinearAlgebra.FreeProduct.lift R A).symm π = π.comp (LinearAlgebra.FreeProduct.ι R A i)
<VAR>I : Type u<VAR>DecidableEq I<VAR>R : Type v<VAR>CommSemiring R<VAR>A : I → Type w<VAR>(i : I) → Semiring (A i)<VAR>(i : I) → Algebra R (A i)<VAR>B : Type w'<VAR>Semiring B<VAR>Algebra R B<VAR>maps : {i : I} → A i →ₐ[R] B<GOAL>(LinearAlgebra.FreeProduct.lift R A) maps = (RingQuot.liftAlgHom R) ⟨(TensorAlgebra.lift R) (DirectSum.toModule R I B fun x => maps.toLinearMap), ⋯⟩
<VAR>I : Type u<VAR>DecidableEq I<VAR>i : I<VAR>R : Type v<VAR>CommSemiring R<VAR>A : I → Type w<VAR>(i : I) → Semiring (A i)<VAR>(i : I) → Algebra R (A i)<VAR>B : Type w'<VAR>Semiring B<VAR>Algebra R B<VAR>maps : {i : I} → A i →ₐ[R] B<GOAL>((LinearAlgebra.FreeProduct.lift R A) fun {i} => maps).comp (LinearAlgebra.FreeProduct.ι R A i) = maps
<VAR>I : Type u<VAR>DecidableEq I<VAR>R : Type v<VAR>CommSemiring R<VAR>A : I → Type w<VAR>(i : I) → Semiring (A i)<VAR>(i : I) → Algebra R (A i)<VAR>B : Type w'<VAR>Semiring B<VAR>Algebra R B<VAR>maps : {i : I} → A i →ₐ[R] B<VAR>f : LinearAlgebra.FreeProduct R A →ₐ[R] B<VAR>h : ∀ (i : I), f.comp (LinearAlgebra.FreeProduct.ι R A i) = maps<GOAL>f = (LinearAlgebra.FreeProduct.lift R A) fun {i} => maps
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>a : A<VAR>p : R[X]<GOAL>p ∈ Polynomial.annIdeal R a ↔ (Polynomial.aeval a) p = 0
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>Field 𝕜<VAR>Ring A<VAR>Algebra 𝕜 A<VAR>a : A<GOAL>Polynomial.annIdealGenerator 𝕜 a = 0 ↔ Polynomial.annIdeal 𝕜 a = ⊥
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>Field 𝕜<VAR>Ring A<VAR>Algebra 𝕜 A<VAR>a : A<GOAL>Ideal.span {Polynomial.annIdealGenerator 𝕜 a} = Polynomial.annIdeal 𝕜 a
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>Field 𝕜<VAR>Ring A<VAR>Algebra 𝕜 A<VAR>a : A<GOAL>Polynomial.annIdealGenerator 𝕜 a ∈ Polynomial.annIdeal 𝕜 a
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>Field 𝕜<VAR>Ring A<VAR>Algebra 𝕜 A<VAR>p : 𝕜[X]<VAR>a : A<GOAL>p ∈ Polynomial.annIdeal 𝕜 a ↔ ∃ s, p = s • Polynomial.annIdealGenerator 𝕜 a
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>Field 𝕜<VAR>Ring A<VAR>Algebra 𝕜 A<VAR>a : A<VAR>hg : Polynomial.annIdealGenerator 𝕜 a ≠ 0<GOAL>(Polynomial.annIdealGenerator 𝕜 a).Monic
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>Field 𝕜<VAR>Ring A<VAR>Algebra 𝕜 A<VAR>a : A<GOAL>(Polynomial.aeval a) (Polynomial.annIdealGenerator 𝕜 a) = 0
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>Field 𝕜<VAR>Ring A<VAR>Algebra 𝕜 A<VAR>p : 𝕜[X]<VAR>a : A<GOAL>p ∈ Polynomial.annIdeal 𝕜 a ↔ Polynomial.annIdealGenerator 𝕜 a ∣ p
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>Field 𝕜<VAR>Ring A<VAR>Algebra 𝕜 A<VAR>a : A<VAR>p : 𝕜[X]<VAR>hp : p ∈ Polynomial.annIdeal 𝕜 a<VAR>hpn0 : p ≠ 0<GOAL>(Polynomial.annIdealGenerator 𝕜 a).degree ≤ p.degree
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>Field 𝕜<VAR>Ring A<VAR>Algebra 𝕜 A<VAR>a : A<GOAL>Polynomial.annIdealGenerator 𝕜 a = minpoly 𝕜 a
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>Field 𝕜<VAR>Ring A<VAR>Algebra 𝕜 A<VAR>a : A<VAR>p : 𝕜[X]<VAR>p_monic : p.Monic<VAR>p_gen : Ideal.span {p} = Polynomial.annIdeal 𝕜 a<GOAL>Polynomial.annIdealGenerator 𝕜 a = p
<VAR>𝕜 : Type u_1<VAR>Field 𝕜<VAR>M : Type u_3<VAR>AddCommGroup M<VAR>Module 𝕜 M<VAR>f : Module.End 𝕜 M<GOAL>Ideal.span {minpoly 𝕜 f} = Module.annihilator 𝕜[X] (Module.AEval' f)
<VAR>R : Type u<VAR>X : Type v<VAR>CommRing R<VAR>Nontrivial R<GOAL>Module.rank R (FreeAlgebra R X) = Cardinal.lift.{u, v} (Cardinal.mk (List X))
<VAR>n : Type u<VAR>DecidableEq n<VAR>Fintype n<VAR>α : Type v<VAR>CommRing α<VAR>StarRing α<VAR>A : Matrix n n α<GOAL>A ∈ Matrix.unitaryGroup n α ↔ A * star A = 1
<VAR>n : Type u<VAR>DecidableEq n<VAR>Fintype n<VAR>α : Type v<VAR>CommRing α<VAR>StarRing α<VAR>A : Matrix n n α<GOAL>A ∈ Matrix.unitaryGroup n α ↔ star A * A = 1
<VAR>n : Type u<VAR>DecidableEq n<VAR>Fintype n<VAR>α : Type v<VAR>CommRing α<VAR>StarRing α<VAR>A : Matrix n n α<VAR>hA : A ∈ Matrix.unitaryGroup n α<GOAL>A.det ∈ unitary α
<VAR>n : Type u<VAR>DecidableEq n<VAR>Fintype n<VAR>α : Type v<VAR>CommRing α<VAR>StarRing α<VAR>A B : ↥(Matrix.unitaryGroup n α)<GOAL>A = B ↔ ∀ (i j : n), ↑A i j = ↑B i j
<VAR>n : Type u<VAR>DecidableEq n<VAR>Fintype n<VAR>α : Type v<VAR>CommRing α<VAR>StarRing α<VAR>A B : ↥(Matrix.unitaryGroup n α)<GOAL>(∀ (i j : n), ↑A i j = ↑B i j) → A = B
<VAR>n : Type u<VAR>DecidableEq n<VAR>Fintype n<VAR>α : Type v<VAR>CommRing α<VAR>StarRing α<VAR>A : ↥(Matrix.unitaryGroup n α)<GOAL>star ↑A * ↑A = 1
<VAR>n : Type u<VAR>DecidableEq n<VAR>Fintype n<VAR>α : Type v<VAR>CommRing α<VAR>StarRing α<VAR>A : ↥(Matrix.unitaryGroup n α)<GOAL>IsUnit (↑A).det
<VAR>n : Type u<VAR>DecidableEq n<VAR>Fintype n<VAR>α : Type v<VAR>CommRing α<VAR>StarRing α<VAR>A : ↥(Matrix.unitaryGroup n α)<GOAL>↑A⁻¹ = star ↑A
<VAR>n : Type u<VAR>DecidableEq n<VAR>Fintype n<VAR>α : Type v<VAR>CommRing α<VAR>StarRing α<VAR>A B : ↥(Matrix.unitaryGroup n α)<GOAL>↑(A * B) = ↑A * ↑B
<VAR>n : Type u<VAR>DecidableEq n<VAR>Fintype n<VAR>α : Type v<VAR>CommRing α<VAR>StarRing α<GOAL>↑1 = 1
<VAR>n : Type u<VAR>DecidableEq n<VAR>Fintype n<VAR>α : Type v<VAR>CommRing α<VAR>StarRing α<VAR>A B : ↥(Matrix.unitaryGroup n α)<GOAL>Matrix.UnitaryGroup.toLin' (A * B) = Matrix.UnitaryGroup.toLin' A ∘ₗ Matrix.UnitaryGroup.toLin' B
<VAR>n : Type u<VAR>DecidableEq n<VAR>Fintype n<VAR>α : Type v<VAR>CommRing α<VAR>StarRing α<GOAL>Matrix.UnitaryGroup.toLin' 1 = LinearMap.id
<VAR>n : Type u<VAR>DecidableEq n<VAR>Fintype n<VAR>α : Type v<VAR>CommRing α<VAR>StarRing α<VAR>A : ↥(Matrix.unitaryGroup n α)<GOAL>↑(Matrix.UnitaryGroup.toGL A) = Matrix.UnitaryGroup.toLin' A
<VAR>n : Type u<VAR>DecidableEq n<VAR>Fintype n<VAR>α : Type v<VAR>CommRing α<VAR>StarRing α<GOAL>Matrix.UnitaryGroup.toGL 1 = 1
<VAR>n : Type u<VAR>DecidableEq n<VAR>Fintype n<VAR>α : Type v<VAR>CommRing α<VAR>StarRing α<VAR>A B : ↥(Matrix.unitaryGroup n α)<GOAL>Matrix.UnitaryGroup.toGL (A * B) = Matrix.UnitaryGroup.toGL A * Matrix.UnitaryGroup.toGL B
<VAR>n : Type u<VAR>DecidableEq n<VAR>Fintype n<VAR>α : Type v<VAR>CommRing α<VAR>StarRing α<VAR>A : Matrix n n α<GOAL>A ∈ Matrix.specialUnitaryGroup n α ↔ A ∈ Matrix.unitaryGroup n α ∧ A.det = 1
<VAR>n : Type u<VAR>DecidableEq n<VAR>Fintype n<VAR>β : Type v<VAR>CommRing β<VAR>A : Matrix n n β<GOAL>A ∈ Matrix.orthogonalGroup n β ↔ A * star A = 1
<VAR>n : Type u<VAR>DecidableEq n<VAR>Fintype n<VAR>β : Type v<VAR>CommRing β<VAR>A : Matrix n n β<GOAL>A ∈ Matrix.orthogonalGroup n β ↔ star A * A = 1
<VAR>n : Type u<VAR>DecidableEq n<VAR>Fintype n<VAR>β : Type v<VAR>CommRing β<VAR>A : Matrix n n β<GOAL>A ∈ Matrix.specialOrthogonalGroup n β ↔ A ∈ Matrix.orthogonalGroup n β ∧ A.det = 1
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>CommSemiring ι<VAR>Module ι (Additive ℤˣ)<VAR>DecidableEq ι<VAR>𝒜 : ι → Type u_5<VAR>ℬ : ι → Type u_6<VAR>CommRing R<VAR>(i : ι) → AddCommGroup (𝒜 i)<VAR>(i : ι) → AddCommGroup (ℬ i)<VAR>(i : ι) → Module R (𝒜 i)<VAR>(i : ι) → Module R (ℬ i)<VAR>i j : ι<VAR>a : 𝒜 i<VAR>b : ℬ j<GOAL>(TensorProduct.gradedCommAux R 𝒜 ℬ) ((DirectSum.lof R (ι × ι) (fun i => 𝒜 i.1 ⊗[R] ℬ i.2) (i, j)) (a ⊗ₜ[R] b)) = (-1) ^ (j * i) • (DirectSum.lof R (ι × ι) (fun i => ℬ i.1 ⊗[R] 𝒜 i.2) (j, i)) (b ⊗ₜ[R] a)
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>CommSemiring ι<VAR>Module ι (Additive ℤˣ)<VAR>DecidableEq ι<VAR>𝒜 : ι → Type u_5<VAR>ℬ : ι → Type u_6<VAR>CommRing R<VAR>(i : ι) → AddCommGroup (𝒜 i)<VAR>(i : ι) → AddCommGroup (ℬ i)<VAR>(i : ι) → Module R (𝒜 i)<VAR>(i : ι) → Module R (ℬ i)<GOAL>TensorProduct.gradedCommAux R 𝒜 ℬ ∘ₗ TensorProduct.gradedCommAux R ℬ 𝒜 = LinearMap.id
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>CommSemiring ι<VAR>Module ι (Additive ℤˣ)<VAR>DecidableEq ι<VAR>𝒜 : ι → Type u_5<VAR>ℬ : ι → Type u_6<VAR>CommRing R<VAR>(i : ι) → AddCommGroup (𝒜 i)<VAR>(i : ι) → AddCommGroup (ℬ i)<VAR>(i : ι) → Module R (𝒜 i)<VAR>(i : ι) → Module R (ℬ i)<GOAL>(TensorProduct.gradedComm R 𝒜 ℬ).symm = TensorProduct.gradedComm R ℬ 𝒜
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>CommSemiring ι<VAR>Module ι (Additive ℤˣ)<VAR>DecidableEq ι<VAR>𝒜 : ι → Type u_5<VAR>ℬ : ι → Type u_6<VAR>CommRing R<VAR>(i : ι) → AddCommGroup (𝒜 i)<VAR>(i : ι) → AddCommGroup (ℬ i)<VAR>(i : ι) → Module R (𝒜 i)<VAR>(i : ι) → Module R (ℬ i)<VAR>DirectSum.GRing 𝒜<VAR>DirectSum.GRing ℬ<VAR>DirectSum.GAlgebra R 𝒜<VAR>DirectSum.GAlgebra R ℬ<VAR>i j : ι<VAR>a : 𝒜 i<VAR>b : ℬ j<GOAL>(TensorProduct.gradedComm R 𝒜 ℬ) ((DirectSum.lof R ι 𝒜 i) a ⊗ₜ[R] (DirectSum.lof R ι ℬ j) b) = (-1) ^ (j * i) • (DirectSum.lof R ι ℬ j) b ⊗ₜ[R] (DirectSum.lof R ι 𝒜 i) a
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>CommSemiring ι<VAR>Module ι (Additive ℤˣ)<VAR>DecidableEq ι<VAR>𝒜 : ι → Type u_5<VAR>ℬ : ι → Type u_6<VAR>CommRing R<VAR>(i : ι) → AddCommGroup (𝒜 i)<VAR>(i : ι) → AddCommGroup (ℬ i)<VAR>(i : ι) → Module R (𝒜 i)<VAR>(i : ι) → Module R (ℬ i)<VAR>DirectSum.GRing 𝒜<VAR>DirectSum.GRing ℬ<VAR>DirectSum.GAlgebra R 𝒜<VAR>DirectSum.GAlgebra R ℬ<VAR>a : ⨁ (i : ι), 𝒜 i<VAR>b : ℬ 0<GOAL>(TensorProduct.gradedComm R 𝒜 ℬ) (a ⊗ₜ[R] (DirectSum.lof R ι ℬ 0) b) = (DirectSum.lof R ι ℬ 0) b ⊗ₜ[R] a
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>CommSemiring ι<VAR>Module ι (Additive ℤˣ)<VAR>DecidableEq ι<VAR>𝒜 : ι → Type u_5<VAR>ℬ : ι → Type u_6<VAR>CommRing R<VAR>(i : ι) → AddCommGroup (𝒜 i)<VAR>(i : ι) → AddCommGroup (ℬ i)<VAR>(i : ι) → Module R (𝒜 i)<VAR>(i : ι) → Module R (ℬ i)<VAR>DirectSum.GRing 𝒜<VAR>DirectSum.GRing ℬ<VAR>DirectSum.GAlgebra R 𝒜<VAR>DirectSum.GAlgebra R ℬ<VAR>a : 𝒜 0<VAR>b : ⨁ (i : ι), ℬ i<GOAL>(TensorProduct.gradedComm R 𝒜 ℬ) ((DirectSum.lof R ι 𝒜 0) a ⊗ₜ[R] b) = b ⊗ₜ[R] (DirectSum.lof R ι 𝒜 0) a
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>CommSemiring ι<VAR>Module ι (Additive ℤˣ)<VAR>DecidableEq ι<VAR>𝒜 : ι → Type u_5<VAR>ℬ : ι → Type u_6<VAR>CommRing R<VAR>(i : ι) → AddCommGroup (𝒜 i)<VAR>(i : ι) → AddCommGroup (ℬ i)<VAR>(i : ι) → Module R (𝒜 i)<VAR>(i : ι) → Module R (ℬ i)<VAR>DirectSum.GRing 𝒜<VAR>DirectSum.GRing ℬ<VAR>DirectSum.GAlgebra R 𝒜<VAR>DirectSum.GAlgebra R ℬ<VAR>a : ⨁ (i : ι), 𝒜 i<GOAL>(TensorProduct.gradedComm R 𝒜 ℬ) (a ⊗ₜ[R] 1) = 1 ⊗ₜ[R] a
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>CommSemiring ι<VAR>Module ι (Additive ℤˣ)<VAR>DecidableEq ι<VAR>𝒜 : ι → Type u_5<VAR>ℬ : ι → Type u_6<VAR>CommRing R<VAR>(i : ι) → AddCommGroup (𝒜 i)<VAR>(i : ι) → AddCommGroup (ℬ i)<VAR>(i : ι) → Module R (𝒜 i)<VAR>(i : ι) → Module R (ℬ i)<VAR>DirectSum.GRing 𝒜<VAR>DirectSum.GRing ℬ<VAR>DirectSum.GAlgebra R 𝒜<VAR>DirectSum.GAlgebra R ℬ<VAR>b : ⨁ (i : ι), ℬ i<GOAL>(TensorProduct.gradedComm R 𝒜 ℬ) (1 ⊗ₜ[R] b) = b ⊗ₜ[R] 1
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>CommSemiring ι<VAR>Module ι (Additive ℤˣ)<VAR>DecidableEq ι<VAR>𝒜 : ι → Type u_5<VAR>ℬ : ι → Type u_6<VAR>CommRing R<VAR>(i : ι) → AddCommGroup (𝒜 i)<VAR>(i : ι) → AddCommGroup (ℬ i)<VAR>(i : ι) → Module R (𝒜 i)<VAR>(i : ι) → Module R (ℬ i)<VAR>DirectSum.GRing 𝒜<VAR>DirectSum.GRing ℬ<VAR>DirectSum.GAlgebra R 𝒜<VAR>DirectSum.GAlgebra R ℬ<GOAL>(TensorProduct.gradedComm R 𝒜 ℬ) 1 = 1
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>CommSemiring ι<VAR>Module ι (Additive ℤˣ)<VAR>DecidableEq ι<VAR>𝒜 : ι → Type u_5<VAR>ℬ : ι → Type u_6<VAR>CommRing R<VAR>(i : ι) → AddCommGroup (𝒜 i)<VAR>(i : ι) → AddCommGroup (ℬ i)<VAR>(i : ι) → Module R (𝒜 i)<VAR>(i : ι) → Module R (ℬ i)<VAR>DirectSum.GRing 𝒜<VAR>DirectSum.GRing ℬ<VAR>DirectSum.GAlgebra R 𝒜<VAR>DirectSum.GAlgebra R ℬ<VAR>a : ⨁ (i : ι), 𝒜 i<VAR>r : R<GOAL>(TensorProduct.gradedComm R 𝒜 ℬ) (a ⊗ₜ[R] (algebraMap R (⨁ (i : ι), ℬ i)) r) = (algebraMap R (⨁ (i : ι), ℬ i)) r ⊗ₜ[R] a
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>CommSemiring ι<VAR>Module ι (Additive ℤˣ)<VAR>DecidableEq ι<VAR>𝒜 : ι → Type u_5<VAR>ℬ : ι → Type u_6<VAR>CommRing R<VAR>(i : ι) → AddCommGroup (𝒜 i)<VAR>(i : ι) → AddCommGroup (ℬ i)<VAR>(i : ι) → Module R (𝒜 i)<VAR>(i : ι) → Module R (ℬ i)<VAR>DirectSum.GRing 𝒜<VAR>DirectSum.GRing ℬ<VAR>DirectSum.GAlgebra R 𝒜<VAR>DirectSum.GAlgebra R ℬ<VAR>r : R<VAR>b : ⨁ (i : ι), ℬ i<GOAL>(TensorProduct.gradedComm R 𝒜 ℬ) ((algebraMap R (⨁ (i : ι), 𝒜 i)) r ⊗ₜ[R] b) = b ⊗ₜ[R] (algebraMap R (⨁ (i : ι), 𝒜 i)) r
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>CommSemiring ι<VAR>Module ι (Additive ℤˣ)<VAR>DecidableEq ι<VAR>𝒜 : ι → Type u_5<VAR>ℬ : ι → Type u_6<VAR>CommRing R<VAR>(i : ι) → AddCommGroup (𝒜 i)<VAR>(i : ι) → AddCommGroup (ℬ i)<VAR>(i : ι) → Module R (𝒜 i)<VAR>(i : ι) → Module R (ℬ i)<VAR>DirectSum.GRing 𝒜<VAR>DirectSum.GRing ℬ<VAR>DirectSum.GAlgebra R 𝒜<VAR>DirectSum.GAlgebra R ℬ<VAR>r : R<GOAL>(TensorProduct.gradedComm R 𝒜 ℬ) ((algebraMap R ((⨁ (i : ι), 𝒜 i) ⊗[R] ⨁ (i : ι), ℬ i)) r) = (algebraMap R ((⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), 𝒜 i)) r
<VAR>R : Type u_7<VAR>ι : Type u_8<VAR>CommSemiring ι<VAR>Module ι (Additive ℤˣ)<VAR>DecidableEq ι<VAR>𝒜 : ι → Type u_9<VAR>ℬ : ι → Type u_10<VAR>CommRing R<VAR>(i : ι) → AddCommGroup (𝒜 i)<VAR>(i : ι) → AddCommGroup (ℬ i)<VAR>(i : ι) → Module R (𝒜 i)<VAR>(i : ι) → Module R (ℬ i)<VAR>DirectSum.GRing 𝒜<VAR>DirectSum.GRing ℬ<VAR>DirectSum.GAlgebra R 𝒜<VAR>DirectSum.GAlgebra R ℬ<GOAL>TensorProduct.gradedMul R 𝒜 ℬ = TensorProduct.curry (TensorProduct.map (LinearMap.mul' R (⨁ (i : ι), 𝒜 i)) (LinearMap.mul' R (⨁ (i : ι), ℬ i)) ∘ₗ ↑(TensorProduct.assoc R (⨁ (i : ι), 𝒜 i) (⨁ (i : ι), 𝒜 i) ((⨁ (i : ι), ℬ i) ⊗[R] ⨁ (i : ι), ℬ i)).symm ∘ₗ LinearMap.lTensor (⨁ (i : ι), 𝒜 i) (↑(TensorProduct.assoc R (⨁ (i : ι), 𝒜 i) (⨁ (i : ι), ℬ i) (⨁ (i : ι), ℬ i)) ∘ₗ LinearMap.rTensor (⨁ (i : ι), ℬ i) ↑(TensorProduct.gradedComm R ℬ 𝒜) ∘ₗ ↑(TensorProduct.assoc R (DirectSum ι ℬ) (DirectSum ι 𝒜) (DirectSum ι ℬ)).symm) ∘ₗ ↑(TensorProduct.assoc R (DirectSum ι 𝒜) (DirectSum ι ℬ) (DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ)))
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>CommSemiring ι<VAR>Module ι (Additive ℤˣ)<VAR>DecidableEq ι<VAR>𝒜 : ι → Type u_5<VAR>ℬ : ι → Type u_6<VAR>CommRing R<VAR>(i : ι) → AddCommGroup (𝒜 i)<VAR>(i : ι) → AddCommGroup (ℬ i)<VAR>(i : ι) → Module R (𝒜 i)<VAR>(i : ι) → Module R (ℬ i)<VAR>DirectSum.GRing 𝒜<VAR>DirectSum.GRing ℬ<VAR>DirectSum.GAlgebra R 𝒜<VAR>DirectSum.GAlgebra R ℬ<VAR>j₁ i₂ : ι<VAR>a₁ : ⨁ (i : ι), 𝒜 i<VAR>b₁ : ℬ j₁<VAR>a₂ : 𝒜 i₂<VAR>b₂ : ⨁ (i : ι), ℬ i<GOAL>((TensorProduct.gradedMul R 𝒜 ℬ) (a₁ ⊗ₜ[R] (DirectSum.lof R ι ℬ j₁) b₁)) ((DirectSum.lof R ι 𝒜 i₂) a₂ ⊗ₜ[R] b₂) = (-1) ^ (j₁ * i₂) • (a₁ * (DirectSum.lof R ι 𝒜 i₂) a₂) ⊗ₜ[R] ((DirectSum.lof R ι ℬ j₁) b₁ * b₂)
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>CommSemiring ι<VAR>Module ι (Additive ℤˣ)<VAR>DecidableEq ι<VAR>𝒜 : ι → Type u_5<VAR>ℬ : ι → Type u_6<VAR>CommRing R<VAR>(i : ι) → AddCommGroup (𝒜 i)<VAR>(i : ι) → AddCommGroup (ℬ i)<VAR>(i : ι) → Module R (𝒜 i)<VAR>(i : ι) → Module R (ℬ i)<VAR>DirectSum.GRing 𝒜<VAR>DirectSum.GRing ℬ<VAR>DirectSum.GAlgebra R 𝒜<VAR>DirectSum.GAlgebra R ℬ<VAR>r : R<VAR>x : (⨁ (i : ι), 𝒜 i) ⊗[R] ⨁ (i : ι), ℬ i<GOAL>((TensorProduct.gradedMul R 𝒜 ℬ) ((algebraMap R (DirectSum ι 𝒜)) r ⊗ₜ[R] 1)) x = r • x
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>CommSemiring ι<VAR>Module ι (Additive ℤˣ)<VAR>DecidableEq ι<VAR>𝒜 : ι → Type u_5<VAR>ℬ : ι → Type u_6<VAR>CommRing R<VAR>(i : ι) → AddCommGroup (𝒜 i)<VAR>(i : ι) → AddCommGroup (ℬ i)<VAR>(i : ι) → Module R (𝒜 i)<VAR>(i : ι) → Module R (ℬ i)<VAR>DirectSum.GRing 𝒜<VAR>DirectSum.GRing ℬ<VAR>DirectSum.GAlgebra R 𝒜<VAR>DirectSum.GAlgebra R ℬ<VAR>x : (⨁ (i : ι), 𝒜 i) ⊗[R] ⨁ (i : ι), ℬ i<GOAL>((TensorProduct.gradedMul R 𝒜 ℬ) 1) x = x
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>CommSemiring ι<VAR>Module ι (Additive ℤˣ)<VAR>DecidableEq ι<VAR>𝒜 : ι → Type u_5<VAR>ℬ : ι → Type u_6<VAR>CommRing R<VAR>(i : ι) → AddCommGroup (𝒜 i)<VAR>(i : ι) → AddCommGroup (ℬ i)<VAR>(i : ι) → Module R (𝒜 i)<VAR>(i : ι) → Module R (ℬ i)<VAR>DirectSum.GRing 𝒜<VAR>DirectSum.GRing ℬ<VAR>DirectSum.GAlgebra R 𝒜<VAR>DirectSum.GAlgebra R ℬ<VAR>x : (⨁ (i : ι), 𝒜 i) ⊗[R] ⨁ (i : ι), ℬ i<VAR>r : R<GOAL>((TensorProduct.gradedMul R 𝒜 ℬ) x) ((algebraMap R (DirectSum ι 𝒜)) r ⊗ₜ[R] 1) = r • x
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>CommSemiring ι<VAR>Module ι (Additive ℤˣ)<VAR>DecidableEq ι<VAR>𝒜 : ι → Type u_5<VAR>ℬ : ι → Type u_6<VAR>CommRing R<VAR>(i : ι) → AddCommGroup (𝒜 i)<VAR>(i : ι) → AddCommGroup (ℬ i)<VAR>(i : ι) → Module R (𝒜 i)<VAR>(i : ι) → Module R (ℬ i)<VAR>DirectSum.GRing 𝒜<VAR>DirectSum.GRing ℬ<VAR>DirectSum.GAlgebra R 𝒜<VAR>DirectSum.GAlgebra R ℬ<VAR>x : (⨁ (i : ι), 𝒜 i) ⊗[R] ⨁ (i : ι), ℬ i<GOAL>((TensorProduct.gradedMul R 𝒜 ℬ) x) 1 = x
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>CommSemiring ι<VAR>Module ι (Additive ℤˣ)<VAR>DecidableEq ι<VAR>𝒜 : ι → Type u_5<VAR>ℬ : ι → Type u_6<VAR>CommRing R<VAR>(i : ι) → AddCommGroup (𝒜 i)<VAR>(i : ι) → AddCommGroup (ℬ i)<VAR>(i : ι) → Module R (𝒜 i)<VAR>(i : ι) → Module R (ℬ i)<VAR>DirectSum.GRing 𝒜<VAR>DirectSum.GRing ℬ<VAR>DirectSum.GAlgebra R 𝒜<VAR>DirectSum.GAlgebra R ℬ<VAR>x y z : DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ<GOAL>((TensorProduct.gradedMul R 𝒜 ℬ) (((TensorProduct.gradedMul R 𝒜 ℬ) x) y)) z = ((TensorProduct.gradedMul R 𝒜 ℬ) x) (((TensorProduct.gradedMul R 𝒜 ℬ) y) z)
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>CommSemiring ι<VAR>Module ι (Additive ℤˣ)<VAR>DecidableEq ι<VAR>𝒜 : ι → Type u_5<VAR>ℬ : ι → Type u_6<VAR>CommRing R<VAR>(i : ι) → AddCommGroup (𝒜 i)<VAR>(i : ι) → AddCommGroup (ℬ i)<VAR>(i : ι) → Module R (𝒜 i)<VAR>(i : ι) → Module R (ℬ i)<VAR>DirectSum.GRing 𝒜<VAR>DirectSum.GRing ℬ<VAR>DirectSum.GAlgebra R 𝒜<VAR>DirectSum.GAlgebra R ℬ<VAR>x y : DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ<GOAL>(TensorProduct.gradedComm R 𝒜 ℬ) (((TensorProduct.gradedMul R 𝒜 ℬ) x) y) = ((TensorProduct.gradedMul R ℬ 𝒜) ((TensorProduct.gradedComm R 𝒜 ℬ) x)) ((TensorProduct.gradedComm R 𝒜 ℬ) y)
<VAR>R : Type u<VAR>S : Type u'<VAR>M : Type v<VAR>N : Type v'<VAR>CommRing R<VAR>CommRing S<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>Module R M<VAR>Module R N<VAR>Algebra R S<VAR>Module S N<VAR>IsScalarTower R S N<VAR>p : Submonoid R<VAR>IsLocalization p S<VAR>f : M →ₗ[R] N<VAR>IsLocalizedModule p f<VAR>hp : p ≤ R⁰<VAR>ι : Type u_1<VAR>v : ι → N<VAR>hf : LinearIndependent S v<GOAL>∃ w, LinearIndependent R w
<VAR>R : Type u<VAR>S : Type u'<VAR>M : Type v<VAR>N : Type v'<VAR>CommRing R<VAR>CommRing S<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>Module R M<VAR>Module R N<VAR>Algebra R S<VAR>Module S N<VAR>IsScalarTower R S N<VAR>p : Submonoid R<VAR>IsLocalization p S<VAR>f : M →ₗ[R] N<VAR>IsLocalizedModule p f<VAR>hp : p ≤ R⁰<GOAL>Cardinal.lift.{v, v'} (Module.rank S N) = Cardinal.lift.{v', v} (Module.rank R M)
<VAR>R : Type u<VAR>S : Type u'<VAR>M : Type v<VAR>CommRing R<VAR>CommRing S<VAR>AddCommGroup M<VAR>Module R M<VAR>Algebra R S<VAR>p : Submonoid R<VAR>IsLocalization p S<VAR>hp : p ≤ R⁰<VAR>N : Type v<VAR>AddCommGroup N<VAR>Module R N<VAR>Module S N<VAR>IsScalarTower R S N<VAR>f : M →ₗ[R] N<VAR>IsLocalizedModule p f<GOAL>Module.rank S N = Module.rank R M
<VAR>R : Type u<VAR>M : Type v<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>IsDomain R<GOAL>∃ s, #↑s = Module.rank R M ∧ LinearIndependent (ι := ↑s) R Subtype.val