ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>m : Type u_2<VAR>α : Type v<VAR>Fintype m<VAR>DecidableEq m<VAR>NonUnitalNonAssocSemiring α<VAR>v w : m → α<VAR>i : m<GOAL>v ⬝ᵥ Matrix.diagonal w i = v i * w i
<VAR>m : Type u_2<VAR>α : Type v<VAR>Fintype m<VAR>DecidableEq m<VAR>NonUnitalNonAssocSemiring α<VAR>v w : m → α<VAR>i : m<GOAL>(v ⬝ᵥ fun j => Matrix.diagonal w j i) = v i * w i
<VAR>m : Type u_2<VAR>α : Type v<VAR>Fintype m<VAR>DecidableEq m<VAR>NonUnitalNonAssocSemiring α<VAR>v : m → α<VAR>x : α<VAR>i : m<GOAL>Pi.single i x ⬝ᵥ v = x * v i
<VAR>m : Type u_2<VAR>α : Type v<VAR>Fintype m<VAR>DecidableEq m<VAR>NonUnitalNonAssocSemiring α<VAR>v : m → α<VAR>x : α<VAR>i : m<GOAL>v ⬝ᵥ Pi.single i x = v i * x
<VAR>n : Type u_3<VAR>α : Type v<VAR>Fintype n<VAR>NonAssocSemiring α<GOAL>1 ⬝ᵥ 1 = ↑(Fintype.card n)
<VAR>m : Type u_2<VAR>α : Type v<VAR>Fintype m<VAR>NonUnitalNonAssocRing α<VAR>v w : m → α<GOAL>-v ⬝ᵥ w = -(v ⬝ᵥ w)
<VAR>m : Type u_2<VAR>α : Type v<VAR>Fintype m<VAR>NonUnitalNonAssocRing α<VAR>v w : m → α<GOAL>v ⬝ᵥ -w = -(v ⬝ᵥ w)
<VAR>m : Type u_2<VAR>α : Type v<VAR>Fintype m<VAR>NonUnitalNonAssocRing α<VAR>v w : m → α<GOAL>-v ⬝ᵥ -w = v ⬝ᵥ w
<VAR>m : Type u_2<VAR>α : Type v<VAR>Fintype m<VAR>NonUnitalNonAssocRing α<VAR>u v w : m → α<GOAL>(u - v) ⬝ᵥ w = u ⬝ᵥ w - v ⬝ᵥ w
<VAR>m : Type u_2<VAR>α : Type v<VAR>Fintype m<VAR>NonUnitalNonAssocRing α<VAR>u v w : m → α<GOAL>u ⬝ᵥ (v - w) = u ⬝ᵥ v - u ⬝ᵥ w
<VAR>m : Type u_2<VAR>R : Type u_7<VAR>α : Type v<VAR>Fintype m<VAR>Monoid R<VAR>Mul α<VAR>AddCommMonoid α<VAR>DistribMulAction R α<VAR>IsScalarTower R α α<VAR>x : R<VAR>v w : m → α<GOAL>x • v ⬝ᵥ w = x • (v ⬝ᵥ w)
<VAR>m : Type u_2<VAR>R : Type u_7<VAR>α : Type v<VAR>Fintype m<VAR>Monoid R<VAR>Mul α<VAR>AddCommMonoid α<VAR>DistribMulAction R α<VAR>SMulCommClass R α α<VAR>x : R<VAR>v w : m → α<GOAL>v ⬝ᵥ x • w = x • (v ⬝ᵥ w)
<VAR>m : Type u_2<VAR>α : Type v<VAR>Fintype m<VAR>NonUnitalSemiring α<VAR>StarRing α<VAR>v w : m → α<GOAL>star v ⬝ᵥ star w = star (w ⬝ᵥ v)
<VAR>m : Type u_2<VAR>α : Type v<VAR>Fintype m<VAR>NonUnitalSemiring α<VAR>StarRing α<VAR>v w : m → α<GOAL>star v ⬝ᵥ w = star (star w ⬝ᵥ v)
<VAR>m : Type u_2<VAR>α : Type v<VAR>Fintype m<VAR>NonUnitalSemiring α<VAR>StarRing α<VAR>v w : m → α<GOAL>v ⬝ᵥ star w = star (w ⬝ᵥ star v)
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type v<VAR>Fintype m<VAR>Mul α<VAR>AddCommMonoid α<VAR>M : Matrix l m α<VAR>N : Matrix m n α<VAR>i : l<VAR>k : n<GOAL>(M * N) i k = ∑ j : m, M i j * N j k
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type v<VAR>Fintype m<VAR>Mul α<VAR>AddCommMonoid α<VAR>M : Matrix l m α<VAR>N : Matrix m n α<VAR>i : l<VAR>k : n<GOAL>(M * N) i k = (fun j => M i j) ⬝ᵥ fun j => N j k
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type v<VAR>β : Type w<VAR>AddCommMonoid α<VAR>i : m<VAR>j : n<VAR>s : Finset β<VAR>g : β → Matrix m n α<GOAL>(∑ c ∈ s, g c) i j = ∑ c ∈ s, g c i j
<VAR>R : Type u_10<VAR>CommRing R<VAR>A B : Matrix (Fin 2) (Fin 2) R<GOAL>(A * B) 0 0 = A 0 0 * B 0 0 + A 0 1 * B 1 0 ∧ (A * B) 0 1 = A 0 0 * B 0 1 + A 0 1 * B 1 1 ∧ (A * B) 1 0 = A 1 0 * B 0 0 + A 1 1 * B 1 0 ∧ (A * B) 1 1 = A 1 0 * B 0 1 + A 1 1 * B 1 1
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>R : Type u_7<VAR>α : Type v<VAR>AddCommMonoid α<VAR>Mul α<VAR>Fintype n<VAR>Monoid R<VAR>DistribMulAction R α<VAR>IsScalarTower R α α<VAR>a : R<VAR>M : Matrix m n α<VAR>N : Matrix n l α<GOAL>a • M * N = a • (M * N)
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>R : Type u_7<VAR>α : Type v<VAR>AddCommMonoid α<VAR>Mul α<VAR>Fintype n<VAR>Monoid R<VAR>DistribMulAction R α<VAR>SMulCommClass R α α<VAR>M : Matrix m n α<VAR>a : R<VAR>N : Matrix n l α<GOAL>M * a • N = a • (M * N)
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>α : Type v<VAR>NonUnitalNonAssocSemiring α<VAR>Fintype n<VAR>M : Matrix m n α<GOAL>M * 0 = 0
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type v<VAR>NonUnitalNonAssocSemiring α<VAR>Fintype m<VAR>M : Matrix m n α<GOAL>0 * M = 0
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>α : Type v<VAR>NonUnitalNonAssocSemiring α<VAR>Fintype n<VAR>L : Matrix m n α<VAR>M N : Matrix n o α<GOAL>L * (M + N) = L * M + L * N
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type v<VAR>NonUnitalNonAssocSemiring α<VAR>Fintype m<VAR>L M : Matrix l m α<VAR>N : Matrix m n α<GOAL>(L + M) * N = L * N + M * N
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type v<VAR>NonUnitalNonAssocSemiring α<VAR>Fintype m<VAR>DecidableEq m<VAR>d : m → α<VAR>M : Matrix m n α<VAR>i : m<VAR>j : n<GOAL>(Matrix.diagonal d * M) i j = d i * M i j
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type v<VAR>NonUnitalNonAssocSemiring α<VAR>Fintype n<VAR>DecidableEq n<VAR>d : n → α<VAR>M : Matrix m n α<VAR>i : m<VAR>j : n<GOAL>(M * Matrix.diagonal d) i j = M i j * d j
<VAR>n : Type u_3<VAR>α : Type v<VAR>NonUnitalNonAssocSemiring α<VAR>Fintype n<VAR>DecidableEq n<VAR>d₁ d₂ : n → α<GOAL>Matrix.diagonal d₁ * Matrix.diagonal d₂ = Matrix.diagonal fun i => d₁ i * d₂ i
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type v<VAR>NonUnitalNonAssocSemiring α<VAR>Fintype m<VAR>DecidableEq m<VAR>M : Matrix m n α<VAR>a : α<GOAL>a • M = (Matrix.diagonal fun x => a) * M
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type v<VAR>NonUnitalNonAssocSemiring α<VAR>Fintype n<VAR>DecidableEq n<VAR>M : Matrix m n α<VAR>a : α<GOAL>MulOpposite.op a • M = M * Matrix.diagonal fun x => a
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type v<VAR>NonUnitalNonAssocSemiring α<VAR>Fintype m<VAR>M : Matrix l m α<VAR>x : Matrix m n α<GOAL>M.addMonoidHomMulLeft x = M * x
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type v<VAR>NonUnitalNonAssocSemiring α<VAR>Fintype m<VAR>M : Matrix m n α<VAR>x : Matrix l m α<GOAL>M.addMonoidHomMulRight x = x * M
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type v<VAR>β : Type w<VAR>NonUnitalNonAssocSemiring α<VAR>Fintype m<VAR>s : Finset β<VAR>f : β → Matrix l m α<VAR>M : Matrix m n α<GOAL>(∑ a ∈ s, f a) * M = ∑ a ∈ s, f a * M
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type v<VAR>β : Type w<VAR>NonUnitalNonAssocSemiring α<VAR>Fintype m<VAR>s : Finset β<VAR>f : β → Matrix m n α<VAR>M : Matrix l m α<GOAL>M * ∑ a ∈ s, f a = ∑ a ∈ s, M * f a
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type v<VAR>NonAssocSemiring α<VAR>Fintype m<VAR>DecidableEq m<VAR>M : Matrix m n α<GOAL>1 * M = M
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type v<VAR>NonAssocSemiring α<VAR>Fintype n<VAR>DecidableEq n<VAR>M : Matrix m n α<GOAL>M * 1 = M
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>α : Type v<VAR>β : Type w<VAR>NonAssocSemiring α<VAR>Fintype n<VAR>L : Matrix m n α<VAR>M : Matrix n o α<VAR>NonAssocSemiring β<VAR>f : α →+* β<GOAL>(L * M).map ⇑f = L.map ⇑f * M.map ⇑f
<VAR>m : Type u_2<VAR>α : Type v<VAR>NonAssocSemiring α<VAR>DecidableEq m<VAR>a : α<GOAL>a • 1 = Matrix.diagonal fun x => a
<VAR>m : Type u_2<VAR>α : Type v<VAR>NonAssocSemiring α<VAR>DecidableEq m<VAR>a : α<GOAL>MulOpposite.op a • 1 = Matrix.diagonal fun x => a
<VAR>n : Type u_3<VAR>α : Type v<VAR>NonAssocSemiring α<VAR>Fintype n<VAR>DecidableEq n<VAR>d : n → α<GOAL>(Matrix.diagonalRingHom n α) d = Matrix.diagonal d
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>α : Type v<VAR>NonUnitalSemiring α<VAR>Fintype m<VAR>Fintype n<VAR>L : Matrix l m α<VAR>M : Matrix m n α<VAR>N : Matrix n o α<GOAL>L * M * N = L * (M * N)
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>α : Type v<VAR>NonUnitalNonAssocRing α<VAR>Fintype n<VAR>M : Matrix m n α<VAR>N : Matrix n o α<GOAL>-M * N = -(M * N)
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>α : Type v<VAR>NonUnitalNonAssocRing α<VAR>Fintype n<VAR>M : Matrix m n α<VAR>N : Matrix n o α<GOAL>M * -N = -(M * N)
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>α : Type v<VAR>NonUnitalNonAssocRing α<VAR>Fintype n<VAR>M M' : Matrix m n α<VAR>N : Matrix n o α<GOAL>(M - M') * N = M * N - M' * N
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>α : Type v<VAR>NonUnitalNonAssocRing α<VAR>Fintype n<VAR>M : Matrix m n α<VAR>N N' : Matrix n o α<GOAL>M * (N - N') = M * N - M * N'
<VAR>n : Type u_3<VAR>α : Type v<VAR>Semiring α<VAR>Fintype n<VAR>DecidableEq n<VAR>v : n → α<VAR>k : ℕ<GOAL>Matrix.diagonal v ^ k = Matrix.diagonal (v ^ k)
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>α : Type v<VAR>Semiring α<VAR>Fintype n<VAR>M : Matrix m n α<VAR>N : Matrix n o α<VAR>a : α<GOAL>(Matrix.of fun i j => a * M i j) * N = a • (M * N)
<VAR>n : Type u_3<VAR>α : Type v<VAR>Semiring α<VAR>DecidableEq n<VAR>Fintype n<VAR>a : α<GOAL>(Matrix.scalar n) a = Matrix.diagonal fun x => a
<VAR>n : Type u_3<VAR>α : Type v<VAR>Semiring α<VAR>DecidableEq n<VAR>Fintype n<VAR>Nonempty n<VAR>r s : α<GOAL>(Matrix.scalar n) r = (Matrix.scalar n) s ↔ r = s
<VAR>n : Type u_3<VAR>α : Type v<VAR>Semiring α<VAR>DecidableEq n<VAR>Fintype n<VAR>r : α<VAR>M : Matrix n n α<GOAL>Commute ((Matrix.scalar n) r) M ↔ r • M = MulOpposite.op r • M
<VAR>n : Type u_3<VAR>α : Type v<VAR>Semiring α<VAR>DecidableEq n<VAR>Fintype n<VAR>r : α<VAR>hr : ∀ (r' : α), Commute r r'<VAR>M : Matrix n n α<GOAL>Commute ((Matrix.scalar n) r) M
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type v<VAR>CommSemiring α<VAR>Fintype n<VAR>DecidableEq n<VAR>M : Matrix m n α<VAR>a : α<GOAL>a • M = M * Matrix.diagonal fun x => a
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>α : Type v<VAR>CommSemiring α<VAR>Fintype n<VAR>M : Matrix m n α<VAR>N : Matrix n o α<VAR>a : α<GOAL>(M * Matrix.of fun i j => a * N i j) = a • (M * N)
<VAR>n : Type u_3<VAR>R : Type u_7<VAR>α : Type v<VAR>Fintype n<VAR>DecidableEq n<VAR>CommSemiring R<VAR>Semiring α<VAR>Algebra R α<VAR>r : R<VAR>i j : n<GOAL>(algebraMap R (Matrix n n α)) r i j = if i = j then (algebraMap R α) r else 0
<VAR>n : Type u_3<VAR>R : Type u_7<VAR>α : Type v<VAR>Fintype n<VAR>DecidableEq n<VAR>CommSemiring R<VAR>Semiring α<VAR>Algebra R α<VAR>r : R<GOAL>(algebraMap R (Matrix n n α)) r = Matrix.diagonal ((algebraMap R (n → α)) r)
<VAR>n : Type u_3<VAR>R : Type u_7<VAR>α : Type v<VAR>Fintype n<VAR>DecidableEq n<VAR>CommSemiring R<VAR>Semiring α<VAR>Algebra R α<GOAL>algebraMap R (Matrix n n α) = (Matrix.diagonalRingHom n α).comp (algebraMap R (n → α))
<VAR>n : Type u_3<VAR>R : Type u_7<VAR>α : Type v<VAR>β : Type w<VAR>Fintype n<VAR>DecidableEq n<VAR>CommSemiring R<VAR>Semiring α<VAR>Semiring β<VAR>Algebra R α<VAR>Algebra R β<VAR>r : R<VAR>f : α → β<VAR>hf : f 0 = 0<VAR>hf₂ : f ((algebraMap R α) r) = (algebraMap R β) r<GOAL>((algebraMap R (Matrix n n α)) r).map f = (algebraMap R (Matrix n n β)) r
<VAR>n : Type u_3<VAR>R : Type u_7<VAR>α : Type v<VAR>Fintype n<VAR>DecidableEq n<VAR>CommSemiring R<VAR>Semiring α<VAR>Algebra R α<VAR>d : n → α<GOAL>(Matrix.diagonalAlgHom R) d = Matrix.diagonal d
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type v<VAR>β : Type w<VAR>f : α ≃ β<VAR>M : Matrix m n α<GOAL>f.mapMatrix M = M.map ⇑f
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type v<GOAL>(Equiv.refl α).mapMatrix = Equiv.refl (Matrix m n α)
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type v<VAR>β : Type w<VAR>f : α ≃ β<GOAL>f.mapMatrix.symm = f.symm.mapMatrix
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type v<VAR>β : Type w<VAR>γ : Type u_9<VAR>f : α ≃ β<VAR>g : β ≃ γ<GOAL>f.mapMatrix.trans g.mapMatrix = (f.trans g).mapMatrix
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type v<VAR>β : Type w<VAR>AddZeroClass α<VAR>AddZeroClass β<VAR>f : α →+ β<VAR>M : Matrix m n α<GOAL>f.mapMatrix M = M.map ⇑f
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type v<VAR>AddZeroClass α<GOAL>(AddMonoidHom.id α).mapMatrix = AddMonoidHom.id (Matrix m n α)
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type v<VAR>β : Type w<VAR>γ : Type u_9<VAR>AddZeroClass α<VAR>AddZeroClass β<VAR>AddZeroClass γ<VAR>f : β →+ γ<VAR>g : α →+ β<GOAL>f.mapMatrix.comp g.mapMatrix = (f.comp g).mapMatrix
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type v<VAR>β : Type w<VAR>Add α<VAR>Add β<VAR>f : α ≃+ β<VAR>M : Matrix m n α<GOAL>f.mapMatrix M = M.map ⇑f
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type v<VAR>Add α<GOAL>(AddEquiv.refl α).mapMatrix = AddEquiv.refl (Matrix m n α)
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type v<VAR>β : Type w<VAR>Add α<VAR>Add β<VAR>f : α ≃+ β<GOAL>f.mapMatrix.symm = f.symm.mapMatrix
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type v<VAR>β : Type w<VAR>γ : Type u_9<VAR>Add α<VAR>Add β<VAR>Add γ<VAR>f : α ≃+ β<VAR>g : β ≃+ γ<GOAL>f.mapMatrix.trans g.mapMatrix = (f.trans g).mapMatrix
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>R : Type u_7<VAR>α : Type v<VAR>β : Type w<VAR>Semiring R<VAR>AddCommMonoid α<VAR>AddCommMonoid β<VAR>Module R α<VAR>Module R β<VAR>f : α →ₗ[R] β<VAR>M : Matrix m n α<GOAL>f.mapMatrix M = M.map ⇑f
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>R : Type u_7<VAR>α : Type v<VAR>Semiring R<VAR>AddCommMonoid α<VAR>Module R α<GOAL>LinearMap.id.mapMatrix = LinearMap.id
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>R : Type u_7<VAR>α : Type v<VAR>β : Type w<VAR>γ : Type u_9<VAR>Semiring R<VAR>AddCommMonoid α<VAR>AddCommMonoid β<VAR>AddCommMonoid γ<VAR>Module R α<VAR>Module R β<VAR>Module R γ<VAR>f : β →ₗ[R] γ<VAR>g : α →ₗ[R] β<GOAL>f.mapMatrix ∘ₗ g.mapMatrix = (f ∘ₗ g).mapMatrix
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>R : Type u_7<VAR>α : Type v<VAR>β : Type w<VAR>Semiring R<VAR>AddCommMonoid α<VAR>AddCommMonoid β<VAR>Module R α<VAR>Module R β<VAR>f : α ≃ₗ[R] β<VAR>M : Matrix m n α<GOAL>f.mapMatrix M = M.map ⇑f
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>R : Type u_7<VAR>α : Type v<VAR>Semiring R<VAR>AddCommMonoid α<VAR>Module R α<GOAL>(LinearEquiv.refl R α).mapMatrix = LinearEquiv.refl R (Matrix m n α)
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>R : Type u_7<VAR>α : Type v<VAR>β : Type w<VAR>Semiring R<VAR>AddCommMonoid α<VAR>AddCommMonoid β<VAR>Module R α<VAR>Module R β<VAR>f : α ≃ₗ[R] β<GOAL>f.mapMatrix.symm = f.symm.mapMatrix
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>R : Type u_7<VAR>α : Type v<VAR>β : Type w<VAR>γ : Type u_9<VAR>Semiring R<VAR>AddCommMonoid α<VAR>AddCommMonoid β<VAR>AddCommMonoid γ<VAR>Module R α<VAR>Module R β<VAR>Module R γ<VAR>f : α ≃ₗ[R] β<VAR>g : β ≃ₗ[R] γ<GOAL>f.mapMatrix ≪≫ₗ g.mapMatrix = (f ≪≫ₗ g).mapMatrix
<VAR>m : Type u_2<VAR>α : Type v<VAR>β : Type w<VAR>Fintype m<VAR>DecidableEq m<VAR>NonAssocSemiring α<VAR>NonAssocSemiring β<VAR>f : α →+* β<VAR>M : Matrix m m α<GOAL>f.mapMatrix M = M.map ⇑f
<VAR>m : Type u_2<VAR>α : Type v<VAR>Fintype m<VAR>DecidableEq m<VAR>NonAssocSemiring α<GOAL>(RingHom.id α).mapMatrix = RingHom.id (Matrix m m α)
<VAR>m : Type u_2<VAR>α : Type v<VAR>β : Type w<VAR>γ : Type u_9<VAR>Fintype m<VAR>DecidableEq m<VAR>NonAssocSemiring α<VAR>NonAssocSemiring β<VAR>NonAssocSemiring γ<VAR>f : β →+* γ<VAR>g : α →+* β<GOAL>f.mapMatrix.comp g.mapMatrix = (f.comp g).mapMatrix
<VAR>m : Type u_2<VAR>α : Type v<VAR>β : Type w<VAR>Fintype m<VAR>DecidableEq m<VAR>NonAssocSemiring α<VAR>NonAssocSemiring β<VAR>f : α ≃+* β<VAR>M : Matrix m m α<GOAL>f.mapMatrix M = M.map ⇑f
<VAR>m : Type u_2<VAR>α : Type v<VAR>Fintype m<VAR>DecidableEq m<VAR>NonAssocSemiring α<GOAL>(RingEquiv.refl α).mapMatrix = RingEquiv.refl (Matrix m m α)
<VAR>m : Type u_2<VAR>α : Type v<VAR>β : Type w<VAR>Fintype m<VAR>DecidableEq m<VAR>NonAssocSemiring α<VAR>NonAssocSemiring β<VAR>f : α ≃+* β<GOAL>f.mapMatrix.symm = f.symm.mapMatrix
<VAR>m : Type u_2<VAR>α : Type v<VAR>β : Type w<VAR>γ : Type u_9<VAR>Fintype m<VAR>DecidableEq m<VAR>NonAssocSemiring α<VAR>NonAssocSemiring β<VAR>NonAssocSemiring γ<VAR>f : α ≃+* β<VAR>g : β ≃+* γ<GOAL>f.mapMatrix.trans g.mapMatrix = (f.trans g).mapMatrix
<VAR>m : Type u_2<VAR>R : Type u_7<VAR>α : Type v<VAR>β : Type w<VAR>Fintype m<VAR>DecidableEq m<VAR>CommSemiring R<VAR>Semiring α<VAR>Semiring β<VAR>Algebra R α<VAR>Algebra R β<VAR>f : α →ₐ[R] β<VAR>M : Matrix m m α<GOAL>f.mapMatrix M = M.map ⇑f
<VAR>m : Type u_2<VAR>R : Type u_7<VAR>α : Type v<VAR>Fintype m<VAR>DecidableEq m<VAR>CommSemiring R<VAR>Semiring α<VAR>Algebra R α<GOAL>(AlgHom.id R α).mapMatrix = AlgHom.id R (Matrix m m α)
<VAR>m : Type u_2<VAR>R : Type u_7<VAR>α : Type v<VAR>β : Type w<VAR>γ : Type u_9<VAR>Fintype m<VAR>DecidableEq m<VAR>CommSemiring R<VAR>Semiring α<VAR>Semiring β<VAR>Semiring γ<VAR>Algebra R α<VAR>Algebra R β<VAR>Algebra R γ<VAR>f : β →ₐ[R] γ<VAR>g : α →ₐ[R] β<GOAL>f.mapMatrix.comp g.mapMatrix = (f.comp g).mapMatrix
<VAR>m : Type u_2<VAR>R : Type u_7<VAR>α : Type v<VAR>β : Type w<VAR>Fintype m<VAR>DecidableEq m<VAR>CommSemiring R<VAR>Semiring α<VAR>Semiring β<VAR>Algebra R α<VAR>Algebra R β<VAR>f : α ≃ₐ[R] β<VAR>M : Matrix m m α<GOAL>f.mapMatrix M = M.map ⇑f
<VAR>m : Type u_2<VAR>R : Type u_7<VAR>α : Type v<VAR>Fintype m<VAR>DecidableEq m<VAR>CommSemiring R<VAR>Semiring α<VAR>Algebra R α<GOAL>AlgEquiv.refl.mapMatrix = AlgEquiv.refl
<VAR>m : Type u_2<VAR>R : Type u_7<VAR>α : Type v<VAR>β : Type w<VAR>Fintype m<VAR>DecidableEq m<VAR>CommSemiring R<VAR>Semiring α<VAR>Semiring β<VAR>Algebra R α<VAR>Algebra R β<VAR>f : α ≃ₐ[R] β<GOAL>f.mapMatrix.symm = f.symm.mapMatrix
<VAR>m : Type u_2<VAR>R : Type u_7<VAR>α : Type v<VAR>β : Type w<VAR>γ : Type u_9<VAR>Fintype m<VAR>DecidableEq m<VAR>CommSemiring R<VAR>Semiring α<VAR>Semiring β<VAR>Semiring γ<VAR>Algebra R α<VAR>Algebra R β<VAR>Algebra R γ<VAR>f : α ≃ₐ[R] β<VAR>g : β ≃ₐ[R] γ<GOAL>f.mapMatrix.trans g.mapMatrix = (f.trans g).mapMatrix
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type v<VAR>Mul α<VAR>w : m → α<VAR>v : n → α<VAR>i : m<VAR>j : n<GOAL>Matrix.vecMulVec w v i j = w i * v j
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type v<VAR>NonUnitalNonAssocSemiring α<VAR>Fintype n<VAR>v : n → α<VAR>M : Matrix m n α<GOAL>∀ (a : m), (Matrix.mulVec.addMonoidHomLeft v) M a = (M *ᵥ v) a
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>α : Type v<VAR>NonUnitalNonAssocSemiring α<VAR>Fintype n<VAR>A : Matrix m n α<VAR>B : Matrix n o α<VAR>i : m<GOAL>(A * B) i = A i ᵥ* B
<VAR>m : Type u_2<VAR>α : Type v<VAR>NonUnitalNonAssocSemiring α<VAR>Fintype m<VAR>DecidableEq m<VAR>v w : m → α<VAR>x : m<GOAL>(Matrix.diagonal v *ᵥ w) x = v x * w x
<VAR>m : Type u_2<VAR>α : Type v<VAR>NonUnitalNonAssocSemiring α<VAR>Fintype m<VAR>DecidableEq m<VAR>v w : m → α<VAR>x : m<GOAL>(v ᵥ* Matrix.diagonal w) x = v x * w x
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>R : Type u_7<VAR>Fintype n<VAR>Fintype m<VAR>NonUnitalSemiring R<VAR>v : m → R<VAR>A : Matrix m n R<VAR>w : n → R<GOAL>v ⬝ᵥ A *ᵥ w = v ᵥ* A ⬝ᵥ w
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type v<VAR>NonUnitalNonAssocSemiring α<VAR>Fintype n<VAR>A : Matrix m n α<GOAL>A *ᵥ 0 = 0
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type v<VAR>NonUnitalNonAssocSemiring α<VAR>Fintype m<VAR>A : Matrix m n α<GOAL>0 ᵥ* A = 0
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type v<VAR>NonUnitalNonAssocSemiring α<VAR>Fintype n<VAR>v : n → α<GOAL>0 *ᵥ v = 0
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type v<VAR>NonUnitalNonAssocSemiring α<VAR>Fintype m<VAR>v : m → α<GOAL>v ᵥ* 0 = 0
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>R : Type u_7<VAR>α : Type v<VAR>NonUnitalNonAssocSemiring α<VAR>Fintype n<VAR>Monoid R<VAR>DistribMulAction R α<VAR>IsScalarTower R α α<VAR>a : R<VAR>A : Matrix m n α<VAR>b : n → α<GOAL>(a • A) *ᵥ b = a • A *ᵥ b
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type v<VAR>NonUnitalNonAssocSemiring α<VAR>Fintype n<VAR>A : Matrix m n α<VAR>x y : n → α<GOAL>A *ᵥ (x + y) = A *ᵥ x + A *ᵥ y
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type v<VAR>NonUnitalNonAssocSemiring α<VAR>Fintype n<VAR>A B : Matrix m n α<VAR>x : n → α<GOAL>(A + B) *ᵥ x = A *ᵥ x + B *ᵥ x
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type v<VAR>NonUnitalNonAssocSemiring α<VAR>Fintype m<VAR>A B : Matrix m n α<VAR>x : m → α<GOAL>x ᵥ* (A + B) = x ᵥ* A + x ᵥ* B
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type v<VAR>NonUnitalNonAssocSemiring α<VAR>Fintype m<VAR>A : Matrix m n α<VAR>x y : m → α<GOAL>(x + y) ᵥ* A = x ᵥ* A + y ᵥ* A
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>R : Type u_7<VAR>S : Type u_8<VAR>Fintype n<VAR>Monoid R<VAR>NonUnitalNonAssocSemiring S<VAR>DistribMulAction R S<VAR>IsScalarTower R S S<VAR>M : Matrix n m S<VAR>b : R<VAR>v : n → S<GOAL>(b • v) ᵥ* M = b • v ᵥ* M
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>R : Type u_7<VAR>S : Type u_8<VAR>Fintype n<VAR>Monoid R<VAR>NonUnitalNonAssocSemiring S<VAR>DistribMulAction R S<VAR>SMulCommClass R S S<VAR>M : Matrix m n S<VAR>b : R<VAR>v : n → S<GOAL>M *ᵥ b • v = b • M *ᵥ v
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>R : Type u_7<VAR>Fintype n<VAR>DecidableEq n<VAR>NonUnitalNonAssocSemiring R<VAR>M : Matrix m n R<VAR>j : n<VAR>x : R<GOAL>M *ᵥ Pi.single j x = fun i => M i j * x
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>R : Type u_7<VAR>Fintype m<VAR>DecidableEq m<VAR>NonUnitalNonAssocSemiring R<VAR>M : Matrix m n R<VAR>i : m<VAR>x : R<GOAL>Pi.single i x ᵥ* M = fun j => x * M i j
<VAR>n : Type u_3<VAR>R : Type u_7<VAR>Fintype n<VAR>DecidableEq n<VAR>NonUnitalNonAssocSemiring R<VAR>v : n → R<VAR>j : n<VAR>x : R<GOAL>Matrix.diagonal v *ᵥ Pi.single j x = Pi.single j (v j * x)
<VAR>n : Type u_3<VAR>R : Type u_7<VAR>Fintype n<VAR>DecidableEq n<VAR>NonUnitalNonAssocSemiring R<VAR>v : n → R<VAR>j : n<VAR>x : R<GOAL>Pi.single j x ᵥ* Matrix.diagonal v = Pi.single j (x * v j)
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>α : Type v<VAR>NonUnitalSemiring α<VAR>Fintype n<VAR>Fintype m<VAR>v : m → α<VAR>M : Matrix m n α<VAR>N : Matrix n o α<GOAL>v ᵥ* M ᵥ* N = v ᵥ* (M * N)
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>α : Type v<VAR>NonUnitalSemiring α<VAR>Fintype n<VAR>Fintype o<VAR>v : o → α<VAR>M : Matrix m n α<VAR>N : Matrix n o α<GOAL>M *ᵥ N *ᵥ v = (M * N) *ᵥ v
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type v<VAR>NonUnitalSemiring α<VAR>Fintype n<VAR>StarRing α<VAR>M : Matrix m n α<VAR>v : n → α<GOAL>star (M *ᵥ v) = star v ᵥ* Mᴴ
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type v<VAR>NonUnitalSemiring α<VAR>Fintype m<VAR>StarRing α<VAR>M : Matrix m n α<VAR>v : m → α<GOAL>star (v ᵥ* M) = Mᴴ *ᵥ star v
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type v<VAR>NonUnitalSemiring α<VAR>Fintype m<VAR>StarRing α<VAR>A : Matrix m n α<VAR>x : m → α<GOAL>Aᴴ *ᵥ x = star (star x ᵥ* A)
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type v<VAR>NonUnitalSemiring α<VAR>Fintype n<VAR>StarRing α<VAR>A : Matrix m n α<VAR>x : n → α<GOAL>x ᵥ* Aᴴ = star (A *ᵥ star x)
<VAR>n : Type u_3<VAR>α : Type v<VAR>NonUnitalSemiring α<VAR>Fintype n<VAR>A B C : Matrix n n α<VAR>i j : n<GOAL>(A * B * C) i j = A i ⬝ᵥ B *ᵥ Cᵀ j
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type v<VAR>NonAssocSemiring α<VAR>Fintype n<VAR>A : Matrix m n α<GOAL>A *ᵥ 1 = fun i => ∑ j : n, A i j
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type v<VAR>NonAssocSemiring α<VAR>Fintype m<VAR>A : Matrix m n α<GOAL>1 ᵥ* A = fun j => ∑ i : m, A i j
<VAR>m : Type u_2<VAR>α : Type v<VAR>NonAssocSemiring α<VAR>Fintype m<VAR>DecidableEq m<VAR>v : m → α<GOAL>1 *ᵥ v = v
<VAR>m : Type u_2<VAR>α : Type v<VAR>NonAssocSemiring α<VAR>Fintype m<VAR>DecidableEq m<VAR>v : m → α<GOAL>v ᵥ* 1 = v
<VAR>m : Type u_2<VAR>α : Type v<VAR>NonAssocSemiring α<VAR>Fintype m<VAR>DecidableEq m<VAR>x : α<VAR>v : m → α<GOAL>(Matrix.diagonal fun x_1 => x) *ᵥ v = x • v
<VAR>m : Type u_2<VAR>α : Type v<VAR>NonAssocSemiring α<VAR>Fintype m<VAR>DecidableEq m<VAR>x : α<VAR>v : m → α<GOAL>(v ᵥ* Matrix.diagonal fun x_1 => x) = MulOpposite.op x • v
<VAR>m : Type u_2<VAR>α : Type v<VAR>NonAssocSemiring α<VAR>Fintype m<VAR>DecidableEq m<VAR>x : ℕ<VAR>v : m → α<GOAL>↑x *ᵥ v = ↑x • v
<VAR>m : Type u_2<VAR>α : Type v<VAR>NonAssocSemiring α<VAR>Fintype m<VAR>DecidableEq m<VAR>x : ℕ<VAR>v : m → α<GOAL>v ᵥ* ↑x = MulOpposite.op ↑x • v
<VAR>m : Type u_2<VAR>α : Type v<VAR>NonAssocSemiring α<VAR>Fintype m<VAR>DecidableEq m<VAR>x : ℕ<VAR>x.AtLeastTwo<VAR>v : m → α<GOAL>OfNat.ofNat x *ᵥ v = OfNat.ofNat x • v
<VAR>m : Type u_2<VAR>α : Type v<VAR>NonAssocSemiring α<VAR>Fintype m<VAR>DecidableEq m<VAR>x : ℕ<VAR>x.AtLeastTwo<VAR>v : m → α<GOAL>v ᵥ* OfNat.ofNat x = MulOpposite.op (OfNat.ofNat x) • v
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type v<VAR>NonUnitalNonAssocRing α<VAR>Fintype m<VAR>v : m → α<VAR>A : Matrix m n α<GOAL>-v ᵥ* A = -(v ᵥ* A)
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type v<VAR>NonUnitalNonAssocRing α<VAR>Fintype m<VAR>v : m → α<VAR>A : Matrix m n α<GOAL>v ᵥ* -A = -(v ᵥ* A)
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type v<VAR>NonUnitalNonAssocRing α<VAR>Fintype m<VAR>v : m → α<VAR>A : Matrix m n α<GOAL>-v ᵥ* -A = v ᵥ* A
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type v<VAR>NonUnitalNonAssocRing α<VAR>Fintype n<VAR>v : n → α<VAR>A : Matrix m n α<GOAL>-A *ᵥ v = -(A *ᵥ v)