ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>m : Type u_3<VAR>n : Type u_4<VAR>Fintype n<VAR>Finite m<VAR>DecidableEq n<VAR>M₁ : Type u_5<VAR>M₂ : Type u_6<VAR>AddCommMonoid M₁<VAR>AddCommMonoid M₂<VAR>Module R M₁<VAR>Module R M₂<VAR>v₁ : Basis n R M₁<VAR>v₂ : Basis m R M₂<VAR>G : Type u_7<VAR>Group G<VAR>DistribMulAction G M₂<VAR>SMulCommClass G R M₂<VAR>g : G<VAR>f : M₁ →ₗ[R] M₂<GOAL>(LinearMap.toMatrix v₁ (g • v₂)) f = (LinearMap.toMatrix v₁ v₂) (DistribMulAction.toLinearMap R M₂ g⁻¹ ∘ₗ f)
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>m : Type u_3<VAR>n : Type u_4<VAR>Fintype n<VAR>Fintype m<VAR>DecidableEq n<VAR>M₁ : Type u_5<VAR>M₂ : Type u_6<VAR>AddCommMonoid M₁<VAR>AddCommMonoid M₂<VAR>Module R M₁<VAR>Module R M₂<VAR>v₁ : Basis n R M₁<VAR>v₂ : Basis m R M₂<VAR>M : Matrix m n R<VAR>v : M₁<GOAL>((Matrix.toLin v₁ v₂) M) v = ∑ j : m, (M *ᵥ ⇑(v₁.repr v)) j • v₂ j
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>m : Type u_3<VAR>n : Type u_4<VAR>Fintype n<VAR>Fintype m<VAR>DecidableEq n<VAR>M₁ : Type u_5<VAR>M₂ : Type u_6<VAR>AddCommMonoid M₁<VAR>AddCommMonoid M₂<VAR>Module R M₁<VAR>Module R M₂<VAR>v₁ : Basis n R M₁<VAR>v₂ : Basis m R M₂<VAR>M : Matrix m n R<VAR>i : n<GOAL>((Matrix.toLin v₁ v₂) M) (v₁ i) = ∑ j : m, M j i • v₂ j
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>l : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>Fintype n<VAR>Fintype m<VAR>DecidableEq n<VAR>M₁ : Type u_5<VAR>M₂ : Type u_6<VAR>AddCommMonoid M₁<VAR>AddCommMonoid M₂<VAR>Module R M₁<VAR>Module R M₂<VAR>v₁ : Basis n R M₁<VAR>v₂ : Basis m R M₂<VAR>M₃ : Type u_7<VAR>AddCommMonoid M₃<VAR>Module R M₃<VAR>v₃ : Basis l R M₃<VAR>Finite l<VAR>DecidableEq m<VAR>f : M₂ →ₗ[R] M₃<VAR>g : M₁ →ₗ[R] M₂<GOAL>(LinearMap.toMatrix v₁ v₃) (f ∘ₗ g) = (LinearMap.toMatrix v₂ v₃) f * (LinearMap.toMatrix v₁ v₂) g
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>n : Type u_4<VAR>Fintype n<VAR>DecidableEq n<VAR>M₁ : Type u_5<VAR>AddCommMonoid M₁<VAR>Module R M₁<VAR>v₁ : Basis n R M₁<VAR>f g : M₁ →ₗ[R] M₁<GOAL>(LinearMap.toMatrix v₁ v₁) (f * g) = (LinearMap.toMatrix v₁ v₁) f * (LinearMap.toMatrix v₁ v₁) g
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>n : Type u_4<VAR>Fintype n<VAR>DecidableEq n<VAR>M₁ : Type u_5<VAR>AddCommMonoid M₁<VAR>Module R M₁<VAR>v₁ : Basis n R M₁<VAR>f : M₁ →ₗ[R] M₁<VAR>k : ℕ<GOAL>(LinearMap.toMatrix v₁ v₁) f ^ k = (LinearMap.toMatrix v₁ v₁) (f ^ k)
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>l : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>Fintype n<VAR>Fintype m<VAR>DecidableEq n<VAR>M₁ : Type u_5<VAR>M₂ : Type u_6<VAR>AddCommMonoid M₁<VAR>AddCommMonoid M₂<VAR>Module R M₁<VAR>Module R M₂<VAR>v₁ : Basis n R M₁<VAR>v₂ : Basis m R M₂<VAR>M₃ : Type u_7<VAR>AddCommMonoid M₃<VAR>Module R M₃<VAR>v₃ : Basis l R M₃<VAR>Finite l<VAR>DecidableEq m<VAR>A : Matrix l m R<VAR>B : Matrix m n R<GOAL>(Matrix.toLin v₁ v₃) (A * B) = (Matrix.toLin v₂ v₃) A ∘ₗ (Matrix.toLin v₁ v₂) B
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>l : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>Fintype n<VAR>Fintype m<VAR>DecidableEq n<VAR>M₁ : Type u_5<VAR>M₂ : Type u_6<VAR>AddCommMonoid M₁<VAR>AddCommMonoid M₂<VAR>Module R M₁<VAR>Module R M₂<VAR>v₁ : Basis n R M₁<VAR>v₂ : Basis m R M₂<VAR>M₃ : Type u_7<VAR>AddCommMonoid M₃<VAR>Module R M₃<VAR>v₃ : Basis l R M₃<VAR>Finite l<VAR>DecidableEq m<VAR>A : Matrix l m R<VAR>B : Matrix m n R<VAR>x : M₁<GOAL>((Matrix.toLin v₁ v₃) (A * B)) x = ((Matrix.toLin v₂ v₃) A) (((Matrix.toLin v₁ v₂) B) x)
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>m : Type u_3<VAR>n : Type u_4<VAR>Fintype n<VAR>Fintype m<VAR>DecidableEq n<VAR>M₁ : Type u_5<VAR>M₂ : Type u_6<VAR>AddCommMonoid M₁<VAR>AddCommMonoid M₂<VAR>Module R M₁<VAR>Module R M₂<VAR>v₁ : Basis n R M₁<VAR>v₂ : Basis m R M₂<VAR>DecidableEq m<VAR>M : Matrix m n R<VAR>M' : Matrix n m R<VAR>hMM' : M * M' = 1<VAR>hM'M : M' * M = 1<VAR>a : M₁<GOAL>(Matrix.toLinOfInv v₁ v₂ hMM' hM'M) a = ((Matrix.toLin v₁ v₂) M) a
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>m : Type u_3<VAR>n : Type u_4<VAR>Fintype n<VAR>Fintype m<VAR>DecidableEq n<VAR>M₁ : Type u_5<VAR>M₂ : Type u_6<VAR>AddCommMonoid M₁<VAR>AddCommMonoid M₂<VAR>Module R M₁<VAR>Module R M₂<VAR>v₁ : Basis n R M₁<VAR>v₂ : Basis m R M₂<VAR>DecidableEq m<VAR>M : Matrix m n R<VAR>M' : Matrix n m R<VAR>hMM' : M * M' = 1<VAR>hM'M : M' * M = 1<VAR>a : M₂<GOAL>(Matrix.toLinOfInv v₁ v₂ hMM' hM'M).symm a = ((Matrix.toLin v₂ v₁) M') a
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>n : Type u_4<VAR>Fintype n<VAR>DecidableEq n<VAR>M₁ : Type u_5<VAR>AddCommMonoid M₁<VAR>Module R M₁<VAR>v₁ : Basis n R M₁<GOAL>(LinearMap.toMatrixAlgEquiv v₁).symm = Matrix.toLinAlgEquiv v₁
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>n : Type u_4<VAR>Fintype n<VAR>DecidableEq n<VAR>M₁ : Type u_5<VAR>AddCommMonoid M₁<VAR>Module R M₁<VAR>v₁ : Basis n R M₁<GOAL>(Matrix.toLinAlgEquiv v₁).symm = LinearMap.toMatrixAlgEquiv v₁
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>n : Type u_4<VAR>Fintype n<VAR>DecidableEq n<VAR>M₁ : Type u_5<VAR>AddCommMonoid M₁<VAR>Module R M₁<VAR>v₁ : Basis n R M₁<VAR>f : M₁ →ₗ[R] M₁<GOAL>(Matrix.toLinAlgEquiv v₁) ((LinearMap.toMatrixAlgEquiv v₁) f) = f
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>n : Type u_4<VAR>Fintype n<VAR>DecidableEq n<VAR>M₁ : Type u_5<VAR>AddCommMonoid M₁<VAR>Module R M₁<VAR>v₁ : Basis n R M₁<VAR>M : Matrix n n R<GOAL>(LinearMap.toMatrixAlgEquiv v₁) ((Matrix.toLinAlgEquiv v₁) M) = M
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>n : Type u_4<VAR>Fintype n<VAR>DecidableEq n<VAR>M₁ : Type u_5<VAR>AddCommMonoid M₁<VAR>Module R M₁<VAR>v₁ : Basis n R M₁<VAR>f : M₁ →ₗ[R] M₁<VAR>i j : n<GOAL>(LinearMap.toMatrixAlgEquiv v₁) f i j = (v₁.repr (f (v₁ j))) i
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>n : Type u_4<VAR>Fintype n<VAR>DecidableEq n<VAR>M₁ : Type u_5<VAR>AddCommMonoid M₁<VAR>Module R M₁<VAR>v₁ : Basis n R M₁<VAR>f : M₁ →ₗ[R] M₁<VAR>j : n<GOAL>((LinearMap.toMatrixAlgEquiv v₁) f)ᵀ j = ⇑(v₁.repr (f (v₁ j)))
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>n : Type u_4<VAR>Fintype n<VAR>DecidableEq n<VAR>M₁ : Type u_5<VAR>AddCommMonoid M₁<VAR>Module R M₁<VAR>v₁ : Basis n R M₁<VAR>M : Matrix n n R<VAR>v : M₁<GOAL>((Matrix.toLinAlgEquiv v₁) M) v = ∑ j : n, (M *ᵥ ⇑(v₁.repr v)) j • v₁ j
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>n : Type u_4<VAR>Fintype n<VAR>DecidableEq n<VAR>M₁ : Type u_5<VAR>AddCommMonoid M₁<VAR>Module R M₁<VAR>v₁ : Basis n R M₁<VAR>M : Matrix n n R<VAR>i : n<GOAL>((Matrix.toLinAlgEquiv v₁) M) (v₁ i) = ∑ j : n, M j i • v₁ j
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>n : Type u_4<VAR>Fintype n<VAR>DecidableEq n<VAR>M₁ : Type u_5<VAR>AddCommMonoid M₁<VAR>Module R M₁<VAR>v₁ : Basis n R M₁<GOAL>(LinearMap.toMatrixAlgEquiv v₁) LinearMap.id = 1
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>n : Type u_4<VAR>Fintype n<VAR>DecidableEq n<VAR>M₁ : Type u_5<VAR>AddCommMonoid M₁<VAR>Module R M₁<VAR>v₁ : Basis n R M₁<GOAL>(Matrix.toLinAlgEquiv v₁) 1 = LinearMap.id
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>n : Type u_4<VAR>Fintype n<VAR>DecidableEq n<VAR>M₁ : Type u_5<VAR>AddCommMonoid M₁<VAR>Module R M₁<VAR>v₁ : Basis n R M₁<VAR>DecidableEq M₁<VAR>f : M₁ →ₗ[R] M₁<VAR>k i : n<GOAL>(LinearMap.toMatrixAlgEquiv v₁.reindexRange) f ⟨v₁ k, ⋯⟩ ⟨v₁ i, ⋯⟩ = (LinearMap.toMatrixAlgEquiv v₁) f k i
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>n : Type u_4<VAR>Fintype n<VAR>DecidableEq n<VAR>M₁ : Type u_5<VAR>AddCommMonoid M₁<VAR>Module R M₁<VAR>v₁ : Basis n R M₁<VAR>f g : M₁ →ₗ[R] M₁<GOAL>(LinearMap.toMatrixAlgEquiv v₁) (f ∘ₗ g) = (LinearMap.toMatrixAlgEquiv v₁) f * (LinearMap.toMatrixAlgEquiv v₁) g
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>n : Type u_4<VAR>Fintype n<VAR>DecidableEq n<VAR>M₁ : Type u_5<VAR>AddCommMonoid M₁<VAR>Module R M₁<VAR>v₁ : Basis n R M₁<VAR>f g : M₁ →ₗ[R] M₁<GOAL>(LinearMap.toMatrixAlgEquiv v₁) (f * g) = (LinearMap.toMatrixAlgEquiv v₁) f * (LinearMap.toMatrixAlgEquiv v₁) g
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>n : Type u_4<VAR>Fintype n<VAR>DecidableEq n<VAR>M₁ : Type u_5<VAR>AddCommMonoid M₁<VAR>Module R M₁<VAR>v₁ : Basis n R M₁<VAR>A B : Matrix n n R<GOAL>(Matrix.toLinAlgEquiv v₁) (A * B) = (Matrix.toLinAlgEquiv v₁) A ∘ₗ (Matrix.toLinAlgEquiv v₁) B
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>a b c d : R<VAR>x : R × R<GOAL>((Matrix.toLin (Basis.finTwoProd R) (Basis.finTwoProd R)) !![a, b; c, d]) x = (a * x.1 + b * x.2, c * x.1 + d * x.2)
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>a b c d : R<GOAL>(Matrix.toLin (Basis.finTwoProd R) (Basis.finTwoProd R)) !![a, b; c, d] = (a • LinearMap.fst R R R + b • LinearMap.snd R R R).prod (c • LinearMap.fst R R R + d • LinearMap.snd R R R)
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>n : Type u_4<VAR>Fintype n<VAR>DecidableEq n<VAR>M₁ : Type u_5<VAR>AddCommMonoid M₁<VAR>Module R M₁<VAR>v₁ : Basis n R M₁<VAR>x : R<GOAL>(LinearMap.toMatrix v₁ v₁) (DistribMulAction.toLinearMap R M₁ x) = Matrix.diagonal fun x_1 => x
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>m : Type u_3<VAR>n : Type u_4<VAR>Fintype n<VAR>Fintype m<VAR>M₁ : Type u_5<VAR>M₂ : Type u_6<VAR>AddCommMonoid M₁<VAR>AddCommMonoid M₂<VAR>Module R M₁<VAR>Module R M₂<VAR>v₁ : Basis n R M₁<VAR>v₂ : Basis m R M₂<VAR>DecidableEq n<VAR>DecidableEq m<VAR>DecidableEq (n ⊕ m)<VAR>φ₁ : Module.End R M₁<VAR>φ₂ : Module.End R M₂<GOAL>(LinearMap.toMatrix (v₁.prod v₂) (v₁.prod v₂)) (LinearMap.prodMap φ₁ φ₂) = Matrix.fromBlocks ((LinearMap.toMatrix v₁ v₁) φ₁) 0 0 ((LinearMap.toMatrix v₂ v₂) φ₂)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>CommRing R<VAR>Ring S<VAR>Algebra R S<VAR>m : Type u_3<VAR>Fintype m<VAR>DecidableEq m<VAR>b : Basis m R S<VAR>x : S<VAR>i j : m<GOAL>(LinearMap.toMatrix b b) ((Algebra.lmul R S) x) i j = (b.repr (x * b j)) i
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>CommRing R<VAR>Ring S<VAR>Algebra R S<VAR>m : Type u_3<VAR>Fintype m<VAR>DecidableEq m<VAR>b : Basis m R S<VAR>x : R<GOAL>(LinearMap.toMatrix b b) ((Algebra.lsmul R R S) x) = Matrix.diagonal fun x_1 => x
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>CommRing R<VAR>Ring S<VAR>Algebra R S<VAR>m : Type u_3<VAR>Fintype m<VAR>DecidableEq m<VAR>b : Basis m R S<VAR>x : S<GOAL>(Algebra.leftMulMatrix b) x = (LinearMap.toMatrix b b) ((Algebra.lmul R S) x)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>CommRing R<VAR>Ring S<VAR>Algebra R S<VAR>m : Type u_3<VAR>Fintype m<VAR>DecidableEq m<VAR>b : Basis m R S<VAR>x : S<VAR>i j : m<GOAL>(Algebra.leftMulMatrix b) x i j = (b.repr (x * b j)) i
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>CommRing R<VAR>Ring S<VAR>Algebra R S<VAR>m : Type u_3<VAR>Fintype m<VAR>DecidableEq m<VAR>b : Basis m R S<VAR>x y : S<GOAL>(Algebra.leftMulMatrix b) x *ᵥ ⇑(b.repr y) = ⇑(b.repr (x * y))
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>CommRing R<VAR>Ring S<VAR>Algebra R S<VAR>m : Type u_3<VAR>Fintype m<VAR>DecidableEq m<VAR>b : Basis m R S<VAR>x : S<GOAL>(LinearMap.toMatrix b b) (LinearMap.mulLeft R x) = (Algebra.leftMulMatrix b) x
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>CommRing R<VAR>Ring S<VAR>Algebra R S<VAR>m : Type u_3<VAR>Fintype m<VAR>DecidableEq m<VAR>b : Basis m R S<GOAL>Function.Injective ⇑(Algebra.leftMulMatrix b)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>CommRing R<VAR>Ring S<VAR>Algebra R S<VAR>m : Type u_3<VAR>Fintype m<VAR>DecidableEq m<VAR>b : Basis m R S<VAR>G : Type u_4<VAR>Group G<VAR>DistribMulAction G S<VAR>SMulCommClass G R S<VAR>SMulCommClass G S S<VAR>g : G<VAR>x : S<GOAL>(Algebra.leftMulMatrix (g • b)) x = (Algebra.leftMulMatrix b) x
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>CommRing R<VAR>CommRing S<VAR>Ring T<VAR>Algebra R S<VAR>Algebra S T<VAR>Algebra R T<VAR>IsScalarTower R S T<VAR>m : Type u_4<VAR>n : Type u_5<VAR>Fintype m<VAR>Fintype n<VAR>DecidableEq m<VAR>DecidableEq n<VAR>b : Basis m R S<VAR>c : Basis n S T<VAR>x : T<VAR>ik jk : m × n<GOAL>(Algebra.leftMulMatrix (b.smulTower c)) x ik jk = (Algebra.leftMulMatrix b) ((Algebra.leftMulMatrix c) x ik.2 jk.2) ik.1 jk.1
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>CommRing R<VAR>CommRing S<VAR>Ring T<VAR>Algebra R S<VAR>Algebra S T<VAR>Algebra R T<VAR>IsScalarTower R S T<VAR>m : Type u_4<VAR>n : Type u_5<VAR>Fintype m<VAR>Fintype n<VAR>DecidableEq m<VAR>DecidableEq n<VAR>b : Basis m R S<VAR>c : Basis n S T<VAR>x : S<GOAL>(Algebra.leftMulMatrix (b.smulTower c)) ((algebraMap S T) x) = Matrix.blockDiagonal fun x_1 => (Algebra.leftMulMatrix b) x
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>CommRing R<VAR>CommRing S<VAR>Ring T<VAR>Algebra R S<VAR>Algebra S T<VAR>Algebra R T<VAR>IsScalarTower R S T<VAR>m : Type u_4<VAR>n : Type u_5<VAR>Fintype m<VAR>Fintype n<VAR>DecidableEq m<VAR>DecidableEq n<VAR>b : Basis m R S<VAR>c : Basis n S T<VAR>x : S<VAR>i j : m<VAR>k : n<GOAL>(Algebra.leftMulMatrix (b.smulTower c)) ((algebraMap S T) x) (i, k) (j, k) = (Algebra.leftMulMatrix b) x i j
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>CommRing R<VAR>CommRing S<VAR>Ring T<VAR>Algebra R S<VAR>Algebra S T<VAR>Algebra R T<VAR>IsScalarTower R S T<VAR>m : Type u_4<VAR>n : Type u_5<VAR>Fintype m<VAR>Fintype n<VAR>DecidableEq m<VAR>DecidableEq n<VAR>b : Basis m R S<VAR>c : Basis n S T<VAR>x : S<VAR>i j : m<VAR>k k' : n<VAR>h : k ≠ k'<GOAL>(Algebra.leftMulMatrix (b.smulTower c)) ((algebraMap S T) x) (i, k) (j, k') = 0
<VAR>R : Type u_1<VAR>M₁ : Type u_3<VAR>M₂ : Type u_4<VAR>ι₁ : Type u_6<VAR>ι₂ : Type u_7<VAR>CommSemiring R<VAR>AddCommMonoid M₁<VAR>AddCommMonoid M₂<VAR>Module R M₁<VAR>Module R M₂<VAR>Fintype ι₁<VAR>Fintype ι₂<VAR>DecidableEq ι₁<VAR>b₁ : Basis ι₁ R M₁<VAR>b₂ : Basis ι₂ R M₂<GOAL>∀ (a : ι₂ × ι₁ →₀ R), (b₁.linearMap b₂).repr.symm a = (Matrix.toLin b₁ b₂) ((Finsupp.total (ι₂ × ι₁) (Matrix ι₂ ι₁ R) R ⇑(Matrix.stdBasis R ι₂ ι₁)) a)
<VAR>R : Type u_1<VAR>M₁ : Type u_3<VAR>M₂ : Type u_4<VAR>ι₁ : Type u_6<VAR>ι₂ : Type u_7<VAR>CommSemiring R<VAR>AddCommMonoid M₁<VAR>AddCommMonoid M₂<VAR>Module R M₁<VAR>Module R M₂<VAR>Fintype ι₁<VAR>Fintype ι₂<VAR>DecidableEq ι₁<VAR>b₁ : Basis ι₁ R M₁<VAR>b₂ : Basis ι₂ R M₂<GOAL>∀ (a : M₁ →ₗ[R] M₂), (b₁.linearMap b₂).repr a = (Matrix.stdBasis R ι₂ ι₁).repr ((LinearMap.toMatrix b₁ b₂) a)
<VAR>R : Type u_1<VAR>M₁ : Type u_3<VAR>M₂ : Type u_4<VAR>ι₁ : Type u_6<VAR>ι₂ : Type u_7<VAR>CommSemiring R<VAR>AddCommMonoid M₁<VAR>AddCommMonoid M₂<VAR>Module R M₁<VAR>Module R M₂<VAR>Fintype ι₁<VAR>Fintype ι₂<VAR>DecidableEq ι₁<VAR>b₁ : Basis ι₁ R M₁<VAR>b₂ : Basis ι₂ R M₂<VAR>ij : ι₂ × ι₁<GOAL>(b₁.linearMap b₂) ij = (Matrix.toLin b₁ b₂) ((Matrix.stdBasis R ι₂ ι₁) ij)
<VAR>R : Type u_1<VAR>M₁ : Type u_3<VAR>M₂ : Type u_4<VAR>ι₁ : Type u_6<VAR>ι₂ : Type u_7<VAR>CommSemiring R<VAR>AddCommMonoid M₁<VAR>AddCommMonoid M₂<VAR>Module R M₁<VAR>Module R M₂<VAR>Fintype ι₁<VAR>Fintype ι₂<VAR>DecidableEq ι₁<VAR>b₁ : Basis ι₁ R M₁<VAR>b₂ : Basis ι₂ R M₂<VAR>ij : ι₂ × ι₁<VAR>k : ι₁<GOAL>((b₁.linearMap b₂) ij) (b₁ k) = if ij.2 = k then b₂ ij.1 else 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>ι : Type u_5<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>Fintype ι<VAR>DecidableEq ι<VAR>b : Basis ι R M<GOAL>∀ (a : M →ₗ[R] M), b.end.repr a = (Matrix.stdBasis R ι ι).repr ((LinearMap.toMatrix b b) a)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>ι : Type u_5<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>Fintype ι<VAR>DecidableEq ι<VAR>b : Basis ι R M<GOAL>∀ (a : ι × ι →₀ R), b.end.repr.symm a = (Matrix.toLin b b) ((Finsupp.total (ι × ι) (Matrix ι ι R) R ⇑(Matrix.stdBasis R ι ι)) a)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>ι : Type u_5<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>Fintype ι<VAR>DecidableEq ι<VAR>b : Basis ι R M<VAR>ij : ι × ι<GOAL>b.end ij = (Matrix.toLin b b) ((Matrix.stdBasis R ι ι) ij)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>ι : Type u_5<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>Fintype ι<VAR>DecidableEq ι<VAR>b : Basis ι R M<VAR>ij : ι × ι<VAR>k : ι<GOAL>(b.end ij) (b k) = if ij.2 = k then b ij.1 else 0
<VAR>ιa : Type u_1<VAR>ιb : Type u_2<VAR>Fintype ιa<VAR>Fintype ιb<VAR>R' : Type u_3<VAR>Mᵢ : Type u_4<VAR>N₁ : Type u_5<VAR>N₂ : Type u_6<VAR>CommSemiring R'<VAR>AddCommGroup N₁<VAR>Module R' N₁<VAR>AddCommGroup N₂<VAR>Module R' N₂<VAR>AddCommMonoid Mᵢ<VAR>Module R' Mᵢ<VAR>DecidableEq ιa<VAR>DecidableEq ιb<VAR>a : Mᵢ [⋀^ιa]→ₗ[R'] N₁<VAR>b : Mᵢ [⋀^ιb]→ₗ[R'] N₂<VAR>σ : Equiv.Perm (ιa ⊕ ιb)<GOAL>AlternatingMap.domCoprod.summand a b (Quotient.mk'' σ) = Equiv.Perm.sign σ • MultilinearMap.domDomCongr σ ((↑a).domCoprod ↑b)
<VAR>ιa : Type u_1<VAR>ιb : Type u_2<VAR>Fintype ιa<VAR>Fintype ιb<VAR>R' : Type u_3<VAR>Mᵢ : Type u_4<VAR>N₁ : Type u_5<VAR>N₂ : Type u_6<VAR>CommSemiring R'<VAR>AddCommGroup N₁<VAR>Module R' N₁<VAR>AddCommGroup N₂<VAR>Module R' N₂<VAR>AddCommMonoid Mᵢ<VAR>Module R' Mᵢ<VAR>DecidableEq ιa<VAR>DecidableEq ιb<VAR>a : Mᵢ [⋀^ιa]→ₗ[R'] N₁<VAR>b : Mᵢ [⋀^ιb]→ₗ[R'] N₂<VAR>σ : Equiv.Perm.ModSumCongr ιa ιb<VAR>v : ιa ⊕ ιb → Mᵢ<VAR>i j : ιa ⊕ ιb<VAR>hv : v i = v j<VAR>hij : i ≠ j<GOAL>(AlternatingMap.domCoprod.summand a b σ) v + (AlternatingMap.domCoprod.summand a b (Equiv.swap i j • σ)) v = 0
<VAR>ιa : Type u_1<VAR>ιb : Type u_2<VAR>Fintype ιa<VAR>Fintype ιb<VAR>R' : Type u_3<VAR>Mᵢ : Type u_4<VAR>N₁ : Type u_5<VAR>N₂ : Type u_6<VAR>CommSemiring R'<VAR>AddCommGroup N₁<VAR>Module R' N₁<VAR>AddCommGroup N₂<VAR>Module R' N₂<VAR>AddCommMonoid Mᵢ<VAR>Module R' Mᵢ<VAR>DecidableEq ιa<VAR>DecidableEq ιb<VAR>a : Mᵢ [⋀^ιa]→ₗ[R'] N₁<VAR>b : Mᵢ [⋀^ιb]→ₗ[R'] N₂<VAR>σ : Equiv.Perm.ModSumCongr ιa ιb<VAR>v : ιa ⊕ ιb → Mᵢ<VAR>i j : ιa ⊕ ιb<VAR>hv : v i = v j<VAR>hij : i ≠ j<GOAL>Equiv.swap i j • σ = σ → (AlternatingMap.domCoprod.summand a b σ) v = 0
<VAR>ιa : Type u_1<VAR>ιb : Type u_2<VAR>Fintype ιa<VAR>Fintype ιb<VAR>R' : Type u_3<VAR>Mᵢ : Type u_4<VAR>N₁ : Type u_5<VAR>N₂ : Type u_6<VAR>CommSemiring R'<VAR>AddCommGroup N₁<VAR>Module R' N₁<VAR>AddCommGroup N₂<VAR>Module R' N₂<VAR>AddCommMonoid Mᵢ<VAR>Module R' Mᵢ<VAR>DecidableEq ιa<VAR>DecidableEq ιb<VAR>a : Mᵢ [⋀^ιa]→ₗ[R'] N₁<VAR>b : Mᵢ [⋀^ιb]→ₗ[R'] N₂<VAR>v : ιa ⊕ ιb → Mᵢ<GOAL>(a.domCoprod b) v = (∑ σ : Equiv.Perm.ModSumCongr ιa ιb, AlternatingMap.domCoprod.summand a b σ) v
<VAR>ιa : Type u_1<VAR>ιb : Type u_2<VAR>Fintype ιa<VAR>Fintype ιb<VAR>R' : Type u_3<VAR>Mᵢ : Type u_4<VAR>N₁ : Type u_5<VAR>N₂ : Type u_6<VAR>CommSemiring R'<VAR>AddCommGroup N₁<VAR>Module R' N₁<VAR>AddCommGroup N₂<VAR>Module R' N₂<VAR>AddCommMonoid Mᵢ<VAR>Module R' Mᵢ<VAR>DecidableEq ιa<VAR>DecidableEq ιb<VAR>a : Mᵢ [⋀^ιa]→ₗ[R'] N₁<VAR>b : Mᵢ [⋀^ιb]→ₗ[R'] N₂<GOAL>↑(a.domCoprod b) = ∑ σ : Equiv.Perm.ModSumCongr ιa ιb, AlternatingMap.domCoprod.summand a b σ
<VAR>ιa : Type u_1<VAR>ιb : Type u_2<VAR>Fintype ιa<VAR>Fintype ιb<VAR>R' : Type u_3<VAR>Mᵢ : Type u_4<VAR>N₁ : Type u_5<VAR>N₂ : Type u_6<VAR>CommSemiring R'<VAR>AddCommGroup N₁<VAR>Module R' N₁<VAR>AddCommGroup N₂<VAR>Module R' N₂<VAR>AddCommMonoid Mᵢ<VAR>Module R' Mᵢ<VAR>DecidableEq ιa<VAR>DecidableEq ιb<VAR>a : Mᵢ [⋀^ιa]→ₗ[R'] N₁<VAR>b : Mᵢ [⋀^ιb]→ₗ[R'] N₂<GOAL>AlternatingMap.domCoprod' (a ⊗ₜ[R'] b) = a.domCoprod b
<VAR>ιa : Type u_1<VAR>ιb : Type u_2<VAR>Fintype ιa<VAR>Fintype ιb<VAR>R' : Type u_3<VAR>Mᵢ : Type u_4<VAR>N₁ : Type u_5<VAR>N₂ : Type u_6<VAR>CommSemiring R'<VAR>AddCommGroup N₁<VAR>Module R' N₁<VAR>AddCommGroup N₂<VAR>Module R' N₂<VAR>AddCommMonoid Mᵢ<VAR>Module R' Mᵢ<VAR>DecidableEq ιa<VAR>DecidableEq ιb<VAR>a : MultilinearMap R' (fun x => Mᵢ) N₁<VAR>b : MultilinearMap R' (fun x => Mᵢ) N₂<GOAL>(↑(MultilinearMap.alternatization a)).domCoprod ↑(MultilinearMap.alternatization b) = ∑ σa : Equiv.Perm ιa, ∑ σb : Equiv.Perm ιb, Equiv.Perm.sign σa • Equiv.Perm.sign σb • (MultilinearMap.domDomCongr σa a).domCoprod (MultilinearMap.domDomCongr σb b)
<VAR>ιa : Type u_1<VAR>ιb : Type u_2<VAR>Fintype ιa<VAR>Fintype ιb<VAR>R' : Type u_3<VAR>Mᵢ : Type u_4<VAR>N₁ : Type u_5<VAR>N₂ : Type u_6<VAR>CommSemiring R'<VAR>AddCommGroup N₁<VAR>Module R' N₁<VAR>AddCommGroup N₂<VAR>Module R' N₂<VAR>AddCommMonoid Mᵢ<VAR>Module R' Mᵢ<VAR>DecidableEq ιa<VAR>DecidableEq ιb<VAR>a : MultilinearMap R' (fun x => Mᵢ) N₁<VAR>b : MultilinearMap R' (fun x => Mᵢ) N₂<GOAL>MultilinearMap.alternatization (a.domCoprod b) = (MultilinearMap.alternatization a).domCoprod (MultilinearMap.alternatization b)
<VAR>ιa : Type u_1<VAR>ιb : Type u_2<VAR>Fintype ιa<VAR>Fintype ιb<VAR>R' : Type u_3<VAR>Mᵢ : Type u_4<VAR>N₁ : Type u_5<VAR>N₂ : Type u_6<VAR>CommSemiring R'<VAR>AddCommGroup N₁<VAR>Module R' N₁<VAR>AddCommGroup N₂<VAR>Module R' N₂<VAR>AddCommMonoid Mᵢ<VAR>Module R' Mᵢ<VAR>DecidableEq ιa<VAR>DecidableEq ιb<VAR>a : Mᵢ [⋀^ιa]→ₗ[R'] N₁<VAR>b : Mᵢ [⋀^ιb]→ₗ[R'] N₂<GOAL>MultilinearMap.alternatization ((↑a).domCoprod ↑b) = ((Fintype.card ιa).factorial * (Fintype.card ιb).factorial) • a.domCoprod b
<VAR>R : Type u<VAR>A : Type v<VAR>CommRing R<VAR>Ring A<VAR>Algebra R A<VAR>IsDomain R<VAR>p : Polynomial R<VAR>a : A<VAR>h : ¬IsUnit ((Polynomial.aeval a) (Multiset.map (fun x => Polynomial.X - Polynomial.C x) p.roots).prod)<GOAL>∃ k ∈ spectrum R a, Polynomial.eval k p = 0
<VAR>𝕜 : Type u<VAR>A : Type v<VAR>Field 𝕜<VAR>Ring A<VAR>Algebra 𝕜 A<VAR>a : A<VAR>p : Polynomial 𝕜<GOAL>(fun x => Polynomial.eval x p) '' spectrum 𝕜 a ⊆ spectrum 𝕜 ((Polynomial.aeval a) p)
<VAR>𝕜 : Type u<VAR>A : Type v<VAR>Field 𝕜<VAR>Ring A<VAR>Algebra 𝕜 A<VAR>IsAlgClosed 𝕜<VAR>a : A<VAR>p : Polynomial 𝕜<VAR>hdeg : 0 < p.degree<GOAL>spectrum 𝕜 ((Polynomial.aeval a) p) = (fun x => Polynomial.eval x p) '' spectrum 𝕜 a
<VAR>𝕜 : Type u<VAR>A : Type v<VAR>Field 𝕜<VAR>Ring A<VAR>Algebra 𝕜 A<VAR>IsAlgClosed 𝕜<VAR>a : A<VAR>p : Polynomial 𝕜<VAR>hnon : (spectrum 𝕜 a).Nonempty<GOAL>spectrum 𝕜 ((Polynomial.aeval a) p) = (fun k => Polynomial.eval k p) '' spectrum 𝕜 a
<VAR>𝕜 : Type u<VAR>A : Type v<VAR>Field 𝕜<VAR>Ring A<VAR>Algebra 𝕜 A<VAR>a : A<VAR>n : ℕ<GOAL>(fun x => x ^ n) '' spectrum 𝕜 a ⊆ spectrum 𝕜 (a ^ n)
<VAR>𝕜 : Type u<VAR>A : Type v<VAR>Field 𝕜<VAR>Ring A<VAR>Algebra 𝕜 A<VAR>IsAlgClosed 𝕜<VAR>a : A<VAR>n : ℕ<VAR>hn : 0 < n<GOAL>spectrum 𝕜 (a ^ n) = (fun x => x ^ n) '' spectrum 𝕜 a
<VAR>𝕜 : Type u<VAR>A : Type v<VAR>Field 𝕜<VAR>Ring A<VAR>Algebra 𝕜 A<VAR>IsAlgClosed 𝕜<VAR>a : A<VAR>ha : (spectrum 𝕜 a).Nonempty<VAR>n : ℕ<GOAL>spectrum 𝕜 (a ^ n) = (fun x => x ^ n) '' spectrum 𝕜 a
<VAR>𝕜 : Type u<VAR>A : Type v<VAR>Field 𝕜<VAR>Ring A<VAR>Algebra 𝕜 A<VAR>IsAlgClosed 𝕜<VAR>Nontrivial A<VAR>I : FiniteDimensional 𝕜 A<VAR>a : A<GOAL>(spectrum 𝕜 a).Nonempty
<VAR>R L : Type u<VAR>CommRing R<VAR>CommRing L<VAR>IsDomain L<VAR>Algebra R L<VAR>NoZeroSMulDivisors R L<VAR>Algebra.IsAlgebraic R L<GOAL>#L ≤ #((p : R[X]) × { x // x ∈ p.aroots L })
<VAR>R L : Type u<VAR>CommRing R<VAR>CommRing L<VAR>IsDomain L<VAR>Algebra R L<VAR>NoZeroSMulDivisors R L<VAR>Algebra.IsAlgebraic R L<GOAL>#L ≤ max #R ℵ₀
<VAR>R : Type u_1<VAR>K : Type u_3<VAR>CommRing R<VAR>Field K<VAR>Algebra R K<VAR>ι : Type u_4<VAR>v : ι → K<VAR>IsAlgClosed K<VAR>hv : IsTranscendenceBasis R v<GOAL>IsAlgClosure (↥(Algebra.adjoin R (Set.range v))) K
<VAR>R K : Type u<VAR>CommRing R<VAR>Field K<VAR>Algebra R K<VAR>IsAlgClosed K<VAR>ι : Type u<VAR>v : ι → K<VAR>hv : IsTranscendenceBasis R v<GOAL>#K ≤ max (max #R #ι) ℵ₀
<VAR>R K : Type u<VAR>CommRing R<VAR>Field K<VAR>Algebra R K<VAR>IsAlgClosed K<VAR>ι : Type u<VAR>v : ι → K<VAR>Nontrivial R<VAR>hv : IsTranscendenceBasis R v<VAR>hR : #R ≤ ℵ₀<VAR>hK : ℵ₀ < #K<GOAL>#K = #ι
<VAR>K L : Type<VAR>Field K<VAR>Field L<VAR>IsAlgClosed K<VAR>IsAlgClosed L<VAR>CharZero K<VAR>CharZero L<VAR>hK : ℵ₀ < #K<VAR>hKL : #K = #L<GOAL>Nonempty (K ≃+* L)
<VAR>K L : Type<VAR>Field K<VAR>Field L<VAR>IsAlgClosed K<VAR>IsAlgClosed L<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>CharP K p<VAR>CharP L p<VAR>hK : ℵ₀ < #K<VAR>hKL : #K = #L<GOAL>Nonempty (K ≃+* L)
<VAR>K L : Type<VAR>Field K<VAR>Field L<VAR>IsAlgClosed K<VAR>IsAlgClosed L<VAR>p : ℕ<VAR>CharP K p<VAR>CharP L p<VAR>hK : ℵ₀ < #K<VAR>hKL : #K = #L<GOAL>Nonempty (K ≃+* L)
<VAR>K : Type u<VAR>CommRing K<GOAL>Function.Injective RatFunc.ofFractionRing
<VAR>K : Type u<VAR>CommRing K<GOAL>Function.Injective RatFunc.toFractionRing
<VAR>K : Type u_1<VAR>CommRing K<VAR>P : Sort u_2<VAR>x : RatFunc K<VAR>f : K[X] → K[X] → P<VAR>H : ∀ {p q p' q' : K[X]}, q ∈ K[X]⁰ → q' ∈ K[X]⁰ → q' * p = q * p' → f p q = f p' q'<GOAL>x.liftOn f H = Localization.liftOn x.toFractionRing (fun p q => f p ↑q) ⋯
<VAR>K : Type u<VAR>CommRing K<VAR>P : Sort v<VAR>n : K[X]<VAR>d : ↥K[X]⁰<VAR>f : K[X] → K[X] → P<VAR>H : ∀ {p q p' q' : K[X]}, q ∈ K[X]⁰ → q' ∈ K[X]⁰ → q' * p = q * p' → f p q = f p' q'<GOAL>{ toFractionRing := Localization.mk n d }.liftOn f H = f n ↑d
<VAR>K : Type u<VAR>CommRing K<VAR>P : Sort v<VAR>f : K[X] → K[X] → P<VAR>H : ∀ {p q a : K[X]}, q ≠ 0 → a ≠ 0 → f (a * p) (a * q) = f p q<VAR>p q p' q' : K[X]<VAR>hq : q ≠ 0<VAR>hq' : q' ≠ 0<VAR>h : q' * p = q * p'<GOAL>f p q = f p' q'