ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>Q : Type u_7<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>AddCommMonoid P<VAR>AddCommMonoid Q<VAR>Module R M<VAR>Module R N<VAR>Module R P<VAR>Module R Q<VAR>g : P ≃ₗ[R] Q<VAR>f : N ≃ₗ[R] P<GOAL>LinearEquiv.rTensor M (f ≪≫ₗ g) = LinearEquiv.rTensor M f ≪≫ₗ LinearEquiv.rTensor M g
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>Q : Type u_7<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>AddCommMonoid P<VAR>AddCommMonoid Q<VAR>Module R M<VAR>Module R N<VAR>Module R P<VAR>Module R Q<VAR>g : P ≃ₗ[R] Q<VAR>f : N ≃ₗ[R] P<VAR>y : TensorProduct R N M<GOAL>(LinearEquiv.rTensor M (f ≪≫ₗ g)) y = (LinearEquiv.rTensor M g) ((LinearEquiv.rTensor M f) y)
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_4<VAR>N : Type u_5<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>Module R M<VAR>Module R N<VAR>f g : N ≃ₗ[R] N<GOAL>LinearEquiv.lTensor M (f * g) = LinearEquiv.lTensor M f * LinearEquiv.lTensor M g
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_4<VAR>N : Type u_5<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>Module R M<VAR>Module R N<VAR>f g : N ≃ₗ[R] N<GOAL>LinearEquiv.rTensor M (f * g) = LinearEquiv.rTensor M f * LinearEquiv.rTensor M g
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_4<VAR>N : Type u_5<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>Module R M<VAR>Module R N<GOAL>LinearEquiv.lTensor M (LinearEquiv.refl R N) = LinearEquiv.refl R (TensorProduct R M N)
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_4<VAR>N : Type u_5<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>Module R M<VAR>Module R N<VAR>x : TensorProduct R M N<GOAL>(LinearEquiv.lTensor M (LinearEquiv.refl R N)) x = x
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_4<VAR>N : Type u_5<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>Module R M<VAR>Module R N<GOAL>LinearEquiv.rTensor M (LinearEquiv.refl R N) = LinearEquiv.refl R (TensorProduct R N M)
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_4<VAR>N : Type u_5<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>Module R M<VAR>Module R N<VAR>y : TensorProduct R N M<GOAL>(LinearEquiv.rTensor M (LinearEquiv.refl R N)) y = y
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>Q : Type u_7<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>AddCommMonoid P<VAR>AddCommMonoid Q<VAR>Module R M<VAR>Module R N<VAR>Module R P<VAR>Module R Q<VAR>f : M ≃ₗ[R] P<VAR>g : N ≃ₗ[R] Q<GOAL>LinearEquiv.rTensor N f ≪≫ₗ LinearEquiv.lTensor P g = TensorProduct.congr f g
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>Q : Type u_7<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>AddCommMonoid P<VAR>AddCommMonoid Q<VAR>Module R M<VAR>Module R N<VAR>Module R P<VAR>Module R Q<VAR>f : M ≃ₗ[R] P<VAR>g : N ≃ₗ[R] Q<GOAL>LinearEquiv.lTensor M g ≪≫ₗ LinearEquiv.rTensor Q f = TensorProduct.congr f g
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>Q : Type u_7<VAR>S : Type u_8<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>AddCommMonoid P<VAR>AddCommMonoid Q<VAR>AddCommMonoid S<VAR>Module R M<VAR>Module R N<VAR>Module R P<VAR>Module R Q<VAR>Module R S<VAR>f : M ≃ₗ[R] P<VAR>g : N ≃ₗ[R] Q<VAR>f' : S ≃ₗ[R] M<GOAL>LinearEquiv.rTensor N f' ≪≫ₗ TensorProduct.congr f g = TensorProduct.congr (f' ≪≫ₗ f) g
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>Q : Type u_7<VAR>S : Type u_8<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>AddCommMonoid P<VAR>AddCommMonoid Q<VAR>AddCommMonoid S<VAR>Module R M<VAR>Module R N<VAR>Module R P<VAR>Module R Q<VAR>Module R S<VAR>f : M ≃ₗ[R] P<VAR>g : N ≃ₗ[R] Q<VAR>g' : S ≃ₗ[R] N<GOAL>LinearEquiv.lTensor M g' ≪≫ₗ TensorProduct.congr f g = TensorProduct.congr f (g' ≪≫ₗ g)
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>Q : Type u_7<VAR>S : Type u_8<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>AddCommMonoid P<VAR>AddCommMonoid Q<VAR>AddCommMonoid S<VAR>Module R M<VAR>Module R N<VAR>Module R P<VAR>Module R Q<VAR>Module R S<VAR>f' : P ≃ₗ[R] S<VAR>f : M ≃ₗ[R] P<VAR>g : N ≃ₗ[R] Q<GOAL>TensorProduct.congr f g ≪≫ₗ LinearEquiv.rTensor Q f' = TensorProduct.congr (f ≪≫ₗ f') g
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>Q : Type u_7<VAR>S : Type u_8<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>AddCommMonoid P<VAR>AddCommMonoid Q<VAR>AddCommMonoid S<VAR>Module R M<VAR>Module R N<VAR>Module R P<VAR>Module R Q<VAR>Module R S<VAR>g' : Q ≃ₗ[R] S<VAR>f : M ≃ₗ[R] P<VAR>g : N ≃ₗ[R] Q<GOAL>TensorProduct.congr f g ≪≫ₗ LinearEquiv.lTensor P g' = TensorProduct.congr f (g ≪≫ₗ g')
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_4<VAR>N : Type u_5<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>Module R M<VAR>Module R N<VAR>f : M ≃ₗ[R] M<VAR>n : ℕ<GOAL>LinearEquiv.rTensor N f ^ n = LinearEquiv.rTensor N (f ^ n)
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_4<VAR>N : Type u_5<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>Module R M<VAR>Module R N<VAR>f : M ≃ₗ[R] M<VAR>n : ℤ<GOAL>LinearEquiv.rTensor N f ^ n = LinearEquiv.rTensor N (f ^ n)
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_4<VAR>N : Type u_5<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>Module R M<VAR>Module R N<VAR>f : N ≃ₗ[R] N<VAR>n : ℕ<GOAL>LinearEquiv.lTensor M f ^ n = LinearEquiv.lTensor M (f ^ n)
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_4<VAR>N : Type u_5<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>Module R M<VAR>Module R N<VAR>f : N ≃ₗ[R] N<VAR>n : ℤ<GOAL>LinearEquiv.lTensor M f ^ n = LinearEquiv.lTensor M (f ^ n)
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_2<VAR>N : Type u_3<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>Module R M<VAR>Module R N<VAR>x : TensorProduct R M N<GOAL>-x + x = 0
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_2<VAR>N : Type u_3<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>Module R M<VAR>Module R N<VAR>m : M<VAR>n : N<GOAL>(-m) ⊗ₜ[R] n = -m ⊗ₜ[R] n
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_2<VAR>N : Type u_3<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>Module R M<VAR>Module R N<VAR>m : M<VAR>n : N<GOAL>m ⊗ₜ[R] (-n) = -m ⊗ₜ[R] n
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_2<VAR>N : Type u_3<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>Module R M<VAR>Module R N<VAR>m : M<VAR>n₁ n₂ : N<GOAL>m ⊗ₜ[R] (n₁ - n₂) = m ⊗ₜ[R] n₁ - m ⊗ₜ[R] n₂
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_2<VAR>N : Type u_3<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>Module R M<VAR>Module R N<VAR>m₁ m₂ : M<VAR>n : N<GOAL>(m₁ - m₂) ⊗ₜ[R] n = m₁ ⊗ₜ[R] n - m₂ ⊗ₜ[R] n
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>AddCommGroup P<VAR>Module R M<VAR>Module R N<VAR>Module R P<VAR>f g : N →ₗ[R] P<GOAL>LinearMap.lTensor M (f - g) = LinearMap.lTensor M f - LinearMap.lTensor M g
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>AddCommGroup P<VAR>Module R M<VAR>Module R N<VAR>Module R P<VAR>f g : N →ₗ[R] P<GOAL>LinearMap.rTensor M (f - g) = LinearMap.rTensor M f - LinearMap.rTensor M g
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>AddCommGroup P<VAR>Module R M<VAR>Module R N<VAR>Module R P<VAR>f : N →ₗ[R] P<GOAL>LinearMap.lTensor M (-f) = -LinearMap.lTensor M f
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>AddCommGroup P<VAR>Module R M<VAR>Module R N<VAR>Module R P<VAR>f : N →ₗ[R] P<GOAL>LinearMap.rTensor M (-f) = -LinearMap.rTensor M f
<VAR>R : Type u_1<VAR>Semiring R<VAR>m : Type u_3<VAR>n : Type u_4<VAR>Fintype m<VAR>M : Matrix m n R<VAR>x : m → R<GOAL>M.vecMulLinear x = x ᵥ* M
<VAR>R : Type u_1<VAR>Semiring R<VAR>m : Type u_3<VAR>n : Type u_4<VAR>Fintype m<VAR>M : Matrix m n R<GOAL>⇑M.vecMulLinear = fun v => v ᵥ* M
<VAR>R : Type u_1<VAR>Semiring R<VAR>m : Type u_3<VAR>n : Type u_4<VAR>Fintype m<VAR>DecidableEq m<VAR>M : Matrix m n R<VAR>i : m<VAR>j : n<GOAL>((LinearMap.stdBasis R (fun x => R) i) 1 ᵥ* M) j = M i j
<VAR>R : Type u_1<VAR>Semiring R<VAR>m : Type u_3<VAR>n : Type u_4<VAR>Fintype m<VAR>M : Matrix m n R<GOAL>LinearMap.range M.vecMulLinear = Submodule.span R (Set.range M)
<VAR>m : Type u_3<VAR>n : Type u_4<VAR>Fintype m<VAR>R : Type u_5<VAR>CommRing R<VAR>M : Matrix m n R<GOAL>(Function.Injective fun v => v ᵥ* M) ↔ LinearIndependent R fun i => M i
<VAR>R : Type u_1<VAR>Semiring R<VAR>m : Type u_3<VAR>n : Type u_4<VAR>Fintype m<VAR>DecidableEq m<VAR>M : Matrix m n R<VAR>v : m → R<GOAL>(Matrix.toLinearMapRight' M) v = v ᵥ* M
<VAR>R : Type u_1<VAR>Semiring R<VAR>l : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>Fintype m<VAR>DecidableEq m<VAR>Fintype l<VAR>DecidableEq l<VAR>M : Matrix l m R<VAR>N : Matrix m n R<GOAL>Matrix.toLinearMapRight' (M * N) = Matrix.toLinearMapRight' N ∘ₗ Matrix.toLinearMapRight' M
<VAR>R : Type u_1<VAR>Semiring R<VAR>l : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>Fintype m<VAR>DecidableEq m<VAR>Fintype l<VAR>DecidableEq l<VAR>M : Matrix l m R<VAR>N : Matrix m n R<VAR>x : l → R<GOAL>(Matrix.toLinearMapRight' (M * N)) x = (Matrix.toLinearMapRight' N) ((Matrix.toLinearMapRight' M) x)
<VAR>R : Type u_1<VAR>Semiring R<VAR>m : Type u_3<VAR>Fintype m<VAR>DecidableEq m<GOAL>Matrix.toLinearMapRight' 1 = LinearMap.id
<VAR>R : Type u_1<VAR>Semiring R<VAR>m : Type u_3<VAR>n : Type u_4<VAR>Fintype m<VAR>DecidableEq m<VAR>Fintype n<VAR>DecidableEq n<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 : n → R<GOAL>∀ (a_1 : m), (Matrix.toLinearEquivRight'OfInv hMM' hM'M) a a_1 = (Matrix.toLinearMapRight' M') a a_1
<VAR>R : Type u_1<VAR>Semiring R<VAR>m : Type u_3<VAR>n : Type u_4<VAR>Fintype m<VAR>DecidableEq m<VAR>Fintype n<VAR>DecidableEq n<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 → R<GOAL>∀ (a_1 : n), (Matrix.toLinearEquivRight'OfInv hMM' hM'M).symm a a_1 = (Matrix.toLinearMapRight' M) a a_1
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>m : Type u_4<VAR>n : Type u_5<VAR>Fintype n<VAR>M : Matrix m n R<GOAL>⇑M.mulVecLin = M.mulVec
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>m : Type u_4<VAR>n : Type u_5<VAR>Fintype n<VAR>M : Matrix m n R<VAR>v : n → R<GOAL>M.mulVecLin v = M *ᵥ v
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>m : Type u_4<VAR>n : Type u_5<VAR>Fintype n<GOAL>Matrix.mulVecLin 0 = 0
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>m : Type u_4<VAR>n : Type u_5<VAR>Fintype n<VAR>M N : Matrix m n R<GOAL>(M + N).mulVecLin = M.mulVecLin + N.mulVecLin
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>m : Type u_4<VAR>n : Type u_5<VAR>Fintype m<VAR>M : Matrix m n R<GOAL>Mᵀ.mulVecLin = M.vecMulLinear
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>m : Type u_4<VAR>n : Type u_5<VAR>Fintype n<VAR>M : Matrix m n R<GOAL>Mᵀ.vecMulLinear = M.mulVecLin
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>k : Type u_2<VAR>l : Type u_3<VAR>m : Type u_4<VAR>n : Type u_5<VAR>Fintype n<VAR>Fintype l<VAR>f₁ : m → k<VAR>e₂ : n ≃ l<VAR>M : Matrix k l R<GOAL>(M.submatrix f₁ ⇑e₂).mulVecLin = LinearMap.funLeft R R f₁ ∘ₗ M.mulVecLin ∘ₗ LinearMap.funLeft R R ⇑e₂.symm
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>k : Type u_2<VAR>l : Type u_3<VAR>m : Type u_4<VAR>n : Type u_5<VAR>Fintype n<VAR>Fintype l<VAR>e₁ : k ≃ m<VAR>e₂ : l ≃ n<VAR>M : Matrix k l R<GOAL>((Matrix.reindex e₁ e₂) M).mulVecLin = ↑(LinearEquiv.funCongrLeft R R e₁.symm) ∘ₗ M.mulVecLin ∘ₗ ↑(LinearEquiv.funCongrLeft R R e₂)
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>n : Type u_5<VAR>Fintype n<VAR>DecidableEq n<GOAL>Matrix.mulVecLin 1 = LinearMap.id
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>l : Type u_3<VAR>m : Type u_4<VAR>n : Type u_5<VAR>Fintype n<VAR>Fintype m<VAR>M : Matrix l m R<VAR>N : Matrix m n R<GOAL>(M * N).mulVecLin = M.mulVecLin ∘ₗ N.mulVecLin
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>m : Type u_4<VAR>n : Type u_5<VAR>Fintype n<VAR>M : Matrix m n R<GOAL>LinearMap.ker M.mulVecLin = ⊥ ↔ ∀ (v : n → R), M *ᵥ v = 0 → v = 0
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>m : Type u_4<VAR>n : Type u_5<VAR>Fintype n<VAR>DecidableEq n<VAR>M : Matrix m n R<VAR>i : m<VAR>j : n<GOAL>(M *ᵥ (LinearMap.stdBasis R (fun x => R) j) 1) i = M i j
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>m : Type u_4<VAR>n : Type u_5<VAR>Fintype n<VAR>DecidableEq n<VAR>M : Matrix m n R<VAR>j : n<GOAL>M *ᵥ (LinearMap.stdBasis R (fun x => R) j) 1 = Mᵀ j
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>m : Type u_4<VAR>n : Type u_5<VAR>Fintype n<VAR>M : Matrix m n R<GOAL>LinearMap.range M.mulVecLin = Submodule.span R (Set.range Mᵀ)
<VAR>m : Type u_4<VAR>n : Type u_5<VAR>Fintype n<VAR>R : Type u_6<VAR>CommRing R<VAR>M : Matrix m n R<GOAL>Function.Injective M.mulVec ↔ LinearIndependent R fun i => Mᵀ i
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>m : Type u_4<VAR>n : Type u_5<VAR>DecidableEq n<VAR>Fintype n<VAR>M : Matrix m n R<GOAL>Matrix.toLin' M = M.mulVecLin
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>m : Type u_4<VAR>n : Type u_5<VAR>DecidableEq n<VAR>Fintype n<GOAL>LinearMap.toMatrix'.symm = Matrix.toLin'
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>m : Type u_4<VAR>n : Type u_5<VAR>DecidableEq n<VAR>Fintype n<GOAL>Matrix.toLin'.symm = LinearMap.toMatrix'
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>m : Type u_4<VAR>n : Type u_5<VAR>DecidableEq n<VAR>Fintype n<VAR>M : Matrix m n R<GOAL>LinearMap.toMatrix' (Matrix.toLin' M) = M
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>m : Type u_4<VAR>n : Type u_5<VAR>DecidableEq n<VAR>Fintype n<VAR>f : (n → R) →ₗ[R] m → R<GOAL>Matrix.toLin' (LinearMap.toMatrix' f) = f
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>m : Type u_4<VAR>n : Type u_5<VAR>DecidableEq n<VAR>Fintype n<VAR>f : (n → R) →ₗ[R] m → R<VAR>i : m<VAR>j : n<GOAL>LinearMap.toMatrix' f i j = f (fun j' => if j' = j then 1 else 0) i
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>m : Type u_4<VAR>n : Type u_5<VAR>DecidableEq n<VAR>Fintype n<VAR>M : Matrix m n R<VAR>v : n → R<GOAL>(Matrix.toLin' M) v = M *ᵥ v
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>n : Type u_5<VAR>DecidableEq n<VAR>Fintype n<GOAL>Matrix.toLin' 1 = LinearMap.id
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>n : Type u_5<VAR>DecidableEq n<VAR>Fintype n<GOAL>LinearMap.toMatrix' LinearMap.id = 1
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>n : Type u_5<VAR>DecidableEq n<VAR>Fintype n<GOAL>LinearMap.toMatrix' 1 = 1
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>l : Type u_3<VAR>m : Type u_4<VAR>n : Type u_5<VAR>DecidableEq n<VAR>Fintype n<VAR>Fintype m<VAR>DecidableEq m<VAR>M : Matrix l m R<VAR>N : Matrix m n R<GOAL>Matrix.toLin' (M * N) = Matrix.toLin' M ∘ₗ Matrix.toLin' N
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>k : Type u_2<VAR>l : Type u_3<VAR>m : Type u_4<VAR>n : Type u_5<VAR>DecidableEq n<VAR>Fintype n<VAR>Fintype l<VAR>DecidableEq l<VAR>f₁ : m → k<VAR>e₂ : n ≃ l<VAR>M : Matrix k l R<GOAL>Matrix.toLin' (M.submatrix f₁ ⇑e₂) = LinearMap.funLeft R R f₁ ∘ₗ Matrix.toLin' M ∘ₗ LinearMap.funLeft R R ⇑e₂.symm
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>k : Type u_2<VAR>l : Type u_3<VAR>m : Type u_4<VAR>n : Type u_5<VAR>DecidableEq n<VAR>Fintype n<VAR>Fintype l<VAR>DecidableEq l<VAR>e₁ : k ≃ m<VAR>e₂ : l ≃ n<VAR>M : Matrix k l R<GOAL>Matrix.toLin' ((Matrix.reindex e₁ e₂) M) = ↑(LinearEquiv.funCongrLeft R R e₁.symm) ∘ₗ Matrix.toLin' M ∘ₗ ↑(LinearEquiv.funCongrLeft R R e₂)
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>l : Type u_3<VAR>m : Type u_4<VAR>n : Type u_5<VAR>DecidableEq n<VAR>Fintype n<VAR>Fintype m<VAR>DecidableEq m<VAR>M : Matrix l m R<VAR>N : Matrix m n R<VAR>x : n → R<GOAL>(Matrix.toLin' (M * N)) x = (Matrix.toLin' M) ((Matrix.toLin' N) x)
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>l : Type u_3<VAR>m : Type u_4<VAR>n : Type u_5<VAR>DecidableEq n<VAR>Fintype n<VAR>Fintype l<VAR>DecidableEq l<VAR>f : (n → R) →ₗ[R] m → R<VAR>g : (l → R) →ₗ[R] n → R<GOAL>LinearMap.toMatrix' (f ∘ₗ g) = LinearMap.toMatrix' f * LinearMap.toMatrix' g
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>m : Type u_4<VAR>Fintype m<VAR>DecidableEq m<VAR>f g : (m → R) →ₗ[R] m → R<GOAL>LinearMap.toMatrix' (f * g) = LinearMap.toMatrix' f * LinearMap.toMatrix' g
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>n : Type u_5<VAR>DecidableEq n<VAR>Fintype n<VAR>x : R<GOAL>LinearMap.toMatrix' ((algebraMap R (Module.End R (n → R))) x) = (Matrix.scalar n) x
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>n : Type u_5<VAR>DecidableEq n<VAR>Fintype n<VAR>M : Matrix n n R<GOAL>LinearMap.ker (Matrix.toLin' M) = ⊥ ↔ ∀ (v : n → R), M *ᵥ v = 0 → v = 0
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>m : Type u_4<VAR>n : Type u_5<VAR>DecidableEq n<VAR>Fintype n<VAR>M : Matrix m n R<GOAL>LinearMap.range (Matrix.toLin' M) = Submodule.span R (Set.range Mᵀ)
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>m : Type u_4<VAR>n : Type u_5<VAR>DecidableEq n<VAR>Fintype n<VAR>Fintype 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 : n → R<GOAL>∀ (a_1 : m), (Matrix.toLin'OfInv hMM' hM'M).symm a a_1 = (Matrix.toLin' M) a a_1
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>m : Type u_4<VAR>n : Type u_5<VAR>DecidableEq n<VAR>Fintype n<VAR>Fintype 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 → R<GOAL>∀ (a_1 : n), (Matrix.toLin'OfInv hMM' hM'M) a a_1 = (Matrix.toLin' M') a a_1
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>n : Type u_5<VAR>DecidableEq n<VAR>Fintype n<GOAL>LinearMap.toMatrixAlgEquiv'.symm = Matrix.toLinAlgEquiv'
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>n : Type u_5<VAR>DecidableEq n<VAR>Fintype n<GOAL>Matrix.toLinAlgEquiv'.symm = LinearMap.toMatrixAlgEquiv'
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>n : Type u_5<VAR>DecidableEq n<VAR>Fintype n<VAR>M : Matrix n n R<GOAL>LinearMap.toMatrixAlgEquiv' (Matrix.toLinAlgEquiv' M) = M
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>n : Type u_5<VAR>DecidableEq n<VAR>Fintype n<VAR>f : (n → R) →ₗ[R] n → R<GOAL>Matrix.toLinAlgEquiv' (LinearMap.toMatrixAlgEquiv' f) = f
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>n : Type u_5<VAR>DecidableEq n<VAR>Fintype n<VAR>f : (n → R) →ₗ[R] n → R<VAR>i j : n<GOAL>LinearMap.toMatrixAlgEquiv' f i j = f (fun j' => if j' = j then 1 else 0) i
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>n : Type u_5<VAR>DecidableEq n<VAR>Fintype n<VAR>M : Matrix n n R<VAR>v : n → R<GOAL>(Matrix.toLinAlgEquiv' M) v = M *ᵥ v
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>n : Type u_5<VAR>DecidableEq n<VAR>Fintype n<GOAL>Matrix.toLinAlgEquiv' 1 = LinearMap.id
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>n : Type u_5<VAR>DecidableEq n<VAR>Fintype n<GOAL>LinearMap.toMatrixAlgEquiv' LinearMap.id = 1
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>n : Type u_5<VAR>DecidableEq n<VAR>Fintype n<VAR>f g : (n → R) →ₗ[R] n → R<GOAL>LinearMap.toMatrixAlgEquiv' (f ∘ₗ g) = LinearMap.toMatrixAlgEquiv' f * LinearMap.toMatrixAlgEquiv' g
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>n : Type u_5<VAR>DecidableEq n<VAR>Fintype n<VAR>f g : (n → R) →ₗ[R] n → R<GOAL>LinearMap.toMatrixAlgEquiv' (f * g) = LinearMap.toMatrixAlgEquiv' f * LinearMap.toMatrixAlgEquiv' g
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>n : Type u_4<VAR>Fintype n<VAR>DecidableEq n<GOAL>LinearMap.toMatrix (Pi.basisFun R n) (Pi.basisFun R n) = LinearMap.toMatrix'
<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<GOAL>Matrix.toLin (Pi.basisFun R n) (Pi.basisFun R m) = Matrix.toLin'
<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₂<GOAL>(LinearMap.toMatrix v₁ v₂).symm = Matrix.toLin v₁ v₂
<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₂<GOAL>(Matrix.toLin v₁ v₂).symm = LinearMap.toMatrix v₁ v₂
<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>f : M₁ →ₗ[R] M₂<GOAL>(Matrix.toLin v₁ v₂) ((LinearMap.toMatrix v₁ v₂) f) = f
<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>M : Matrix m n R<GOAL>(LinearMap.toMatrix v₁ v₂) ((Matrix.toLin v₁ v₂) M) = M
<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>f : M₁ →ₗ[R] M₂<VAR>i : m<VAR>j : n<GOAL>(LinearMap.toMatrix v₁ v₂) f i j = (v₂.repr (f (v₁ j))) i
<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>f : M₁ →ₗ[R] M₂<VAR>j : n<GOAL>((LinearMap.toMatrix v₁ 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₁<GOAL>(LinearMap.toMatrix v₁ 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>(LinearMap.toMatrix v₁ v₁) 1 = 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.toLin v₁ v₁) 1 = LinearMap.id
<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>DecidableEq M₁<VAR>f : M₁ →ₗ[R] M₂<VAR>k : m<VAR>i : n<GOAL>(LinearMap.toMatrix v₁.reindexRange v₂.reindexRange) f ⟨v₂ k, ⋯⟩ ⟨v₁ i, ⋯⟩ = (LinearMap.toMatrix v₁ 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>x : R<GOAL>(LinearMap.toMatrix v₁ v₁) ((algebraMap R (Module.End R M₁)) x) = (Matrix.scalar n) x
<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>f : M₁ →ₗ[R] M₂<VAR>x : M₁<GOAL>(LinearMap.toMatrix v₁ v₂) f *ᵥ ⇑(v₁.repr x) = ⇑(v₂.repr (f x))
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>l : Type u_2<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>Fintype l<VAR>DecidableEq l<VAR>b : Basis l R M₁<VAR>b' : Basis l R M₂<GOAL>(LinearMap.toMatrix b' b) ↑(b'.equiv b (Equiv.refl l)) = 1
<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 (g • v₁) v₂) f = (LinearMap.toMatrix v₁ v₂) (f ∘ₗ DistribMulAction.toLinearMap R M₁ g)