ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>R : Type u_5<VAR>Fintype n<VAR>CommRing R<VAR>A : Matrix m n R<GOAL>A.rank = FiniteDimensional.finrank R ↥(Submodule.span R (Set.range Aᵀ))
<VAR>m : Type u_2<VAR>R : Type u_5<VAR>Field R<VAR>Fintype m<VAR>DecidableEq m<VAR>DecidableEq R<VAR>w : m → R<GOAL>(Matrix.diagonal w).rank = Fintype.card { i // w i ≠ 0 }
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>R : Type u_5<VAR>Fintype n<VAR>Fintype m<VAR>Field R<VAR>PartialOrder R<VAR>StarRing R<VAR>StarOrderedRing R<VAR>A : Matrix m n R<GOAL>LinearMap.ker (Aᴴ * A).mulVecLin = LinearMap.ker A.mulVecLin
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>R : Type u_5<VAR>Fintype n<VAR>Fintype m<VAR>Field R<VAR>PartialOrder R<VAR>StarRing R<VAR>StarOrderedRing R<VAR>A : Matrix m n R<GOAL>(Aᴴ * A).rank = A.rank
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>R : Type u_5<VAR>Fintype n<VAR>Fintype m<VAR>Field R<VAR>PartialOrder R<VAR>StarRing R<VAR>StarOrderedRing R<VAR>A : Matrix m n R<GOAL>Aᴴ.rank = A.rank
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>R : Type u_5<VAR>Fintype n<VAR>Fintype m<VAR>Field R<VAR>PartialOrder R<VAR>StarRing R<VAR>StarOrderedRing R<VAR>A : Matrix m n R<GOAL>(A * Aᴴ).rank = A.rank
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>R : Type u_5<VAR>Fintype n<VAR>Fintype m<VAR>LinearOrderedField R<VAR>A : Matrix m n R<GOAL>LinearMap.ker (Aᵀ * A).mulVecLin = LinearMap.ker A.mulVecLin
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>R : Type u_5<VAR>Fintype n<VAR>Fintype m<VAR>LinearOrderedField R<VAR>A : Matrix m n R<GOAL>(Aᵀ * A).rank = A.rank
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>R : Type u_5<VAR>Fintype n<VAR>Fintype m<VAR>LinearOrderedField R<VAR>A : Matrix m n R<GOAL>Aᵀ.rank = A.rank
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>R : Type u_5<VAR>Fintype n<VAR>Fintype m<VAR>LinearOrderedField R<VAR>A : Matrix m n R<GOAL>(A * Aᵀ).rank = A.rank
<VAR>m : Type u_2<VAR>n : Type u_3<VAR>R : Type u_5<VAR>Fintype n<VAR>LinearOrderedField R<VAR>Finite m<VAR>A : Matrix m n R<GOAL>A.rank = FiniteDimensional.finrank R ↥(Submodule.span R (Set.range A))
<VAR>α : Type u_2<VAR>β : Type u_4<VAR>γ : Type u_6<VAR>l : Type u_8<VAR>m : Type u_9<VAR>n : Type u_10<VAR>p : Type u_11<VAR>f : α → β → γ<VAR>A : Matrix l m α<VAR>B : Matrix n p β<VAR>i : l × n<VAR>j : m × p<GOAL>Matrix.kroneckerMap f A B i j = f (A i.1 j.1) (B i.2 j.2)
<VAR>α : Type u_2<VAR>β : Type u_4<VAR>γ : Type u_6<VAR>l : Type u_8<VAR>m : Type u_9<VAR>n : Type u_10<VAR>p : Type u_11<VAR>f : α → β → γ<VAR>A : Matrix l m α<VAR>B : Matrix n p β<GOAL>Matrix.kroneckerMap f A.transpose B.transpose = (Matrix.kroneckerMap f A B).transpose
<VAR>α : Type u_2<VAR>α' : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_6<VAR>l : Type u_8<VAR>m : Type u_9<VAR>n : Type u_10<VAR>p : Type u_11<VAR>f : α' → β → γ<VAR>g : α → α'<VAR>A : Matrix l m α<VAR>B : Matrix n p β<GOAL>Matrix.kroneckerMap f (A.map g) B = Matrix.kroneckerMap (fun a b => f (g a) b) A B
<VAR>α : Type u_2<VAR>β : Type u_4<VAR>β' : Type u_5<VAR>γ : Type u_6<VAR>l : Type u_8<VAR>m : Type u_9<VAR>n : Type u_10<VAR>p : Type u_11<VAR>f : α → β' → γ<VAR>g : β → β'<VAR>A : Matrix l m α<VAR>B : Matrix n p β<GOAL>Matrix.kroneckerMap f A (B.map g) = Matrix.kroneckerMap (fun a b => f a (g b)) A B
<VAR>α : Type u_2<VAR>β : Type u_4<VAR>γ : Type u_6<VAR>γ' : Type u_7<VAR>l : Type u_8<VAR>m : Type u_9<VAR>n : Type u_10<VAR>p : Type u_11<VAR>f : α → β → γ<VAR>g : γ → γ'<VAR>A : Matrix l m α<VAR>B : Matrix n p β<GOAL>(Matrix.kroneckerMap f A B).map g = Matrix.kroneckerMap (fun a b => g (f a b)) A B
<VAR>α : Type u_2<VAR>β : Type u_4<VAR>γ : Type u_6<VAR>l : Type u_8<VAR>m : Type u_9<VAR>n : Type u_10<VAR>p : Type u_11<VAR>Zero α<VAR>Zero γ<VAR>f : α → β → γ<VAR>hf : ∀ (b : β), f 0 b = 0<VAR>B : Matrix n p β<GOAL>Matrix.kroneckerMap f 0 B = 0
<VAR>α : Type u_2<VAR>β : Type u_4<VAR>γ : Type u_6<VAR>l : Type u_8<VAR>m : Type u_9<VAR>n : Type u_10<VAR>p : Type u_11<VAR>Zero β<VAR>Zero γ<VAR>f : α → β → γ<VAR>hf : ∀ (a : α), f a 0 = 0<VAR>A : Matrix l m α<GOAL>Matrix.kroneckerMap f A 0 = 0
<VAR>α : Type u_2<VAR>β : Type u_4<VAR>γ : Type u_6<VAR>l : Type u_8<VAR>m : Type u_9<VAR>n : Type u_10<VAR>p : Type u_11<VAR>Add α<VAR>Add γ<VAR>f : α → β → γ<VAR>hf : ∀ (a₁ a₂ : α) (b : β), f (a₁ + a₂) b = f a₁ b + f a₂ b<VAR>A₁ A₂ : Matrix l m α<VAR>B : Matrix n p β<GOAL>Matrix.kroneckerMap f (A₁ + A₂) B = Matrix.kroneckerMap f A₁ B + Matrix.kroneckerMap f A₂ B
<VAR>α : Type u_2<VAR>β : Type u_4<VAR>γ : Type u_6<VAR>l : Type u_8<VAR>m : Type u_9<VAR>n : Type u_10<VAR>p : Type u_11<VAR>Add β<VAR>Add γ<VAR>f : α → β → γ<VAR>hf : ∀ (a : α) (b₁ b₂ : β), f a (b₁ + b₂) = f a b₁ + f a b₂<VAR>A : Matrix l m α<VAR>B₁ B₂ : Matrix n p β<GOAL>Matrix.kroneckerMap f A (B₁ + B₂) = Matrix.kroneckerMap f A B₁ + Matrix.kroneckerMap f A B₂
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>β : Type u_4<VAR>γ : Type u_6<VAR>l : Type u_8<VAR>m : Type u_9<VAR>n : Type u_10<VAR>p : Type u_11<VAR>SMul R α<VAR>SMul R γ<VAR>f : α → β → γ<VAR>r : R<VAR>hf : ∀ (a : α) (b : β), f (r • a) b = r • f a b<VAR>A : Matrix l m α<VAR>B : Matrix n p β<GOAL>Matrix.kroneckerMap f (r • A) B = r • Matrix.kroneckerMap f A B
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>β : Type u_4<VAR>γ : Type u_6<VAR>l : Type u_8<VAR>m : Type u_9<VAR>n : Type u_10<VAR>p : Type u_11<VAR>SMul R β<VAR>SMul R γ<VAR>f : α → β → γ<VAR>r : R<VAR>hf : ∀ (a : α) (b : β), f a (r • b) = r • f a b<VAR>A : Matrix l m α<VAR>B : Matrix n p β<GOAL>Matrix.kroneckerMap f A (r • B) = r • Matrix.kroneckerMap f A B
<VAR>α : Type u_2<VAR>β : Type u_4<VAR>γ : Type u_6<VAR>m : Type u_9<VAR>n : Type u_10<VAR>Zero α<VAR>Zero β<VAR>Zero γ<VAR>DecidableEq m<VAR>DecidableEq n<VAR>f : α → β → γ<VAR>hf₁ : ∀ (b : β), f 0 b = 0<VAR>hf₂ : ∀ (a : α), f a 0 = 0<VAR>a : m → α<VAR>b : n → β<GOAL>Matrix.kroneckerMap f (Matrix.diagonal a) (Matrix.diagonal b) = Matrix.diagonal fun mn => f (a mn.1) (b mn.2)
<VAR>α : Type u_2<VAR>β : Type u_4<VAR>γ : Type u_6<VAR>l : Type u_8<VAR>m : Type u_9<VAR>n : Type u_10<VAR>Zero β<VAR>Zero γ<VAR>DecidableEq n<VAR>f : α → β → γ<VAR>hf : ∀ (a : α), f a 0 = 0<VAR>A : Matrix l m α<VAR>b : n → β<GOAL>Matrix.kroneckerMap f A (Matrix.diagonal b) = Matrix.blockDiagonal fun i => A.map fun a => f a (b i)
<VAR>α : Type u_2<VAR>β : Type u_4<VAR>γ : Type u_6<VAR>l : Type u_8<VAR>m : Type u_9<VAR>n : Type u_10<VAR>Zero α<VAR>Zero γ<VAR>DecidableEq l<VAR>f : α → β → γ<VAR>hf : ∀ (b : β), f 0 b = 0<VAR>a : l → α<VAR>B : Matrix m n β<GOAL>Matrix.kroneckerMap f (Matrix.diagonal a) B = (Matrix.reindex (Equiv.prodComm m l) (Equiv.prodComm n l)) (Matrix.blockDiagonal fun i => B.map fun b => f (a i) b)
<VAR>α : Type u_2<VAR>β : Type u_4<VAR>γ : Type u_6<VAR>m : Type u_9<VAR>n : Type u_10<VAR>Zero α<VAR>Zero β<VAR>Zero γ<VAR>One α<VAR>One β<VAR>One γ<VAR>DecidableEq m<VAR>DecidableEq n<VAR>f : α → β → γ<VAR>hf₁ : ∀ (b : β), f 0 b = 0<VAR>hf₂ : ∀ (a : α), f a 0 = 0<VAR>hf₃ : f 1 1 = 1<GOAL>Matrix.kroneckerMap f 1 1 = 1
<VAR>α : Type u_2<VAR>β : Type u_4<VAR>γ : Type u_6<VAR>l : Type u_8<VAR>m : Type u_9<VAR>n : Type u_10<VAR>p : Type u_11<VAR>l' : Type u_14<VAR>m' : Type u_15<VAR>n' : Type u_16<VAR>p' : Type u_17<VAR>f : α → β → γ<VAR>el : l ≃ l'<VAR>em : m ≃ m'<VAR>en : n ≃ n'<VAR>ep : p ≃ p'<VAR>M : Matrix l m α<VAR>N : Matrix n p β<GOAL>Matrix.kroneckerMap f ((Matrix.reindex el em) M) ((Matrix.reindex en ep) N) = (Matrix.reindex (el.prodCongr en) (em.prodCongr ep)) (Matrix.kroneckerMap f M N)
<VAR>α : Type u_2<VAR>β : Type u_4<VAR>γ : Type u_6<VAR>l : Type u_8<VAR>m : Type u_9<VAR>n : Type u_10<VAR>l' : Type u_14<VAR>m' : Type u_15<VAR>n' : Type u_16<VAR>f : α → β → γ<VAR>el : l ≃ l'<VAR>em : m ≃ m'<VAR>M : Matrix l m α<VAR>N : Matrix n n' β<GOAL>Matrix.kroneckerMap f ((Matrix.reindex el em) M) N = (Matrix.reindex (el.prodCongr (Equiv.refl n)) (em.prodCongr (Equiv.refl n'))) (Matrix.kroneckerMap f M N)
<VAR>α : Type u_2<VAR>β : Type u_4<VAR>γ : Type u_6<VAR>l : Type u_8<VAR>m : Type u_9<VAR>n : Type u_10<VAR>l' : Type u_14<VAR>m' : Type u_15<VAR>n' : Type u_16<VAR>f : α → β → γ<VAR>em : m ≃ m'<VAR>en : n ≃ n'<VAR>M : Matrix l l' α<VAR>N : Matrix m n β<GOAL>Matrix.kroneckerMap f M ((Matrix.reindex em en) N) = (Matrix.reindex ((Equiv.refl l).prodCongr em) ((Equiv.refl l').prodCongr en)) (Matrix.kroneckerMap f M N)
<VAR>α : Type u_2<VAR>β : Type u_4<VAR>γ : Type u_6<VAR>l : Type u_8<VAR>m : Type u_9<VAR>n : Type u_10<VAR>p : Type u_11<VAR>q : Type u_12<VAR>r : Type u_13<VAR>δ : Type u_18<VAR>ξ : Type u_19<VAR>ω : Type u_20<VAR>ω' : Type u_21<VAR>f : α → β → γ<VAR>g : γ → δ → ω<VAR>f' : α → ξ → ω'<VAR>g' : β → δ → ξ<VAR>A : Matrix l m α<VAR>B : Matrix n p β<VAR>D : Matrix q r δ<VAR>φ : ω ≃ ω'<VAR>hφ : ∀ (a : α) (b : β) (d : δ), φ (g (f a b) d) = f' a (g' b d)<GOAL>((Matrix.reindex (Equiv.prodAssoc l n q) (Equiv.prodAssoc m p r)).trans φ.mapMatrix) (Matrix.kroneckerMap g (Matrix.kroneckerMap f A B) D) = Matrix.kroneckerMap f' A (Matrix.kroneckerMap g' B D)
<VAR>α : Type u_2<VAR>β : Type u_4<VAR>γ : Type u_6<VAR>l : Type u_8<VAR>m : Type u_9<VAR>n : Type u_10<VAR>p : Type u_11<VAR>q : Type u_12<VAR>r : Type u_13<VAR>δ : Type u_18<VAR>ξ : Type u_19<VAR>ω : Type u_20<VAR>f : α → β → γ<VAR>g : γ → δ → ω<VAR>f' : α → ξ → ω<VAR>g' : β → δ → ξ<VAR>A : Matrix l m α<VAR>B : Matrix n p β<VAR>D : Matrix q r δ<VAR>h : ∀ (a : α) (b : β) (d : δ), g (f a b) d = f' a (g' b d)<GOAL>(Matrix.reindex (Equiv.prodAssoc l n q) (Equiv.prodAssoc m p r)) (Matrix.kroneckerMap g (Matrix.kroneckerMap f A B) D) = Matrix.kroneckerMap f' A (Matrix.kroneckerMap g' B D)
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>β : Type u_4<VAR>γ : Type u_6<VAR>l : Type u_8<VAR>m : Type u_9<VAR>n : Type u_10<VAR>p : Type u_11<VAR>CommSemiring R<VAR>AddCommMonoid α<VAR>AddCommMonoid β<VAR>AddCommMonoid γ<VAR>Module R α<VAR>Module R β<VAR>Module R γ<VAR>f : α →ₗ[R] β →ₗ[R] γ<GOAL>∀ (m_1 : Matrix l m α) (B : Matrix n p β), ((Matrix.kroneckerMapBilinear f) m_1) B = Matrix.kroneckerMap (fun r s => (f r) s) m_1 B
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>β : Type u_4<VAR>γ : Type u_6<VAR>l : Type u_8<VAR>m : Type u_9<VAR>n : Type u_10<VAR>l' : Type u_14<VAR>m' : Type u_15<VAR>n' : Type u_16<VAR>CommSemiring R<VAR>Fintype m<VAR>Fintype m'<VAR>NonUnitalNonAssocSemiring α<VAR>NonUnitalNonAssocSemiring β<VAR>NonUnitalNonAssocSemiring γ<VAR>Module R α<VAR>Module R β<VAR>Module R γ<VAR>f : α →ₗ[R] β →ₗ[R] γ<VAR>h_comm : ∀ (a b : α) (a' b' : β), (f (a * b)) (a' * b') = (f a) a' * (f b) b'<VAR>A : Matrix l m α<VAR>B : Matrix m n α<VAR>A' : Matrix l' m' β<VAR>B' : Matrix m' n' β<GOAL>((Matrix.kroneckerMapBilinear f) (A * B)) (A' * B') = ((Matrix.kroneckerMapBilinear f) A) A' * ((Matrix.kroneckerMapBilinear f) B) B'
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>β : Type u_4<VAR>γ : Type u_6<VAR>m : Type u_9<VAR>n : Type u_10<VAR>CommSemiring R<VAR>Fintype m<VAR>Fintype n<VAR>AddCommMonoid α<VAR>AddCommMonoid β<VAR>AddCommMonoid γ<VAR>Module R α<VAR>Module R β<VAR>Module R γ<VAR>f : α →ₗ[R] β →ₗ[R] γ<VAR>A : Matrix m m α<VAR>B : Matrix n n β<GOAL>(((Matrix.kroneckerMapBilinear f) A) B).trace = (f A.trace) B.trace
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>β : Type u_4<VAR>γ : Type u_6<VAR>m : Type u_9<VAR>n : Type u_10<VAR>CommSemiring R<VAR>Fintype m<VAR>Fintype n<VAR>DecidableEq m<VAR>DecidableEq n<VAR>CommRing α<VAR>CommRing β<VAR>CommRing γ<VAR>Module R α<VAR>Module R β<VAR>Module R γ<VAR>f : α →ₗ[R] β →ₗ[R] γ<VAR>h_comm : ∀ (a b : α) (a' b' : β), (f (a * b)) (a' * b') = (f a) a' * (f b) b'<VAR>A : Matrix m m α<VAR>B : Matrix n n β<GOAL>(((Matrix.kroneckerMapBilinear f) A) B).det = (A.map fun a => (f a) 1).det ^ Fintype.card n * (B.map fun b => (f 1) b).det ^ Fintype.card m
<VAR>α : Type u_2<VAR>l : Type u_8<VAR>m : Type u_9<VAR>n : Type u_10<VAR>p : Type u_11<VAR>Mul α<VAR>A : Matrix l m α<VAR>B : Matrix n p α<VAR>i₁ : l<VAR>i₂ : n<VAR>j₁ : m<VAR>j₂ : p<GOAL>Matrix.kroneckerMap (fun x x_1 => x * x_1) A B (i₁, i₂) (j₁, j₂) = A i₁ j₁ * B i₂ j₂
<VAR>α : Type u_2<VAR>l : Type u_8<VAR>m : Type u_9<VAR>n : Type u_10<VAR>p : Type u_11<VAR>MulZeroClass α<VAR>B : Matrix n p α<GOAL>Matrix.kroneckerMap (fun x x_1 => x * x_1) 0 B = 0
<VAR>α : Type u_2<VAR>l : Type u_8<VAR>m : Type u_9<VAR>n : Type u_10<VAR>p : Type u_11<VAR>MulZeroClass α<VAR>A : Matrix l m α<GOAL>Matrix.kroneckerMap (fun x x_1 => x * x_1) A 0 = 0
<VAR>α : Type u_2<VAR>l : Type u_8<VAR>m : Type u_9<VAR>n : Type u_10<VAR>p : Type u_11<VAR>Distrib α<VAR>A₁ A₂ : Matrix l m α<VAR>B : Matrix n p α<GOAL>Matrix.kroneckerMap (fun x x_1 => x * x_1) (A₁ + A₂) B = Matrix.kroneckerMap (fun x x_1 => x * x_1) A₁ B + Matrix.kroneckerMap (fun x x_1 => x * x_1) A₂ B
<VAR>α : Type u_2<VAR>l : Type u_8<VAR>m : Type u_9<VAR>n : Type u_10<VAR>p : Type u_11<VAR>Distrib α<VAR>A : Matrix l m α<VAR>B₁ B₂ : Matrix n p α<GOAL>Matrix.kroneckerMap (fun x x_1 => x * x_1) A (B₁ + B₂) = Matrix.kroneckerMap (fun x x_1 => x * x_1) A B₁ + Matrix.kroneckerMap (fun x x_1 => x * x_1) A B₂
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>l : Type u_8<VAR>m : Type u_9<VAR>n : Type u_10<VAR>p : Type u_11<VAR>Monoid R<VAR>Monoid α<VAR>MulAction R α<VAR>IsScalarTower R α α<VAR>r : R<VAR>A : Matrix l m α<VAR>B : Matrix n p α<GOAL>Matrix.kroneckerMap (fun x x_1 => x * x_1) (r • A) B = r • Matrix.kroneckerMap (fun x x_1 => x * x_1) A B
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>l : Type u_8<VAR>m : Type u_9<VAR>n : Type u_10<VAR>p : Type u_11<VAR>Monoid R<VAR>Monoid α<VAR>MulAction R α<VAR>SMulCommClass R α α<VAR>r : R<VAR>A : Matrix l m α<VAR>B : Matrix n p α<GOAL>Matrix.kroneckerMap (fun x x_1 => x * x_1) A (r • B) = r • Matrix.kroneckerMap (fun x x_1 => x * x_1) A B
<VAR>α : Type u_2<VAR>m : Type u_9<VAR>n : Type u_10<VAR>MulZeroClass α<VAR>DecidableEq m<VAR>DecidableEq n<VAR>a : m → α<VAR>b : n → α<GOAL>Matrix.kroneckerMap (fun x x_1 => x * x_1) (Matrix.diagonal a) (Matrix.diagonal b) = Matrix.diagonal fun mn => a mn.1 * b mn.2
<VAR>α : Type u_2<VAR>l : Type u_8<VAR>m : Type u_9<VAR>n : Type u_10<VAR>MulZeroClass α<VAR>DecidableEq n<VAR>A : Matrix l m α<VAR>b : n → α<GOAL>Matrix.kroneckerMap (fun x x_1 => x * x_1) A (Matrix.diagonal b) = Matrix.blockDiagonal fun i => MulOpposite.op (b i) • A
<VAR>α : Type u_2<VAR>l : Type u_8<VAR>m : Type u_9<VAR>n : Type u_10<VAR>MulZeroClass α<VAR>DecidableEq l<VAR>a : l → α<VAR>B : Matrix m n α<GOAL>Matrix.kroneckerMap (fun x x_1 => x * x_1) (Matrix.diagonal a) B = (Matrix.reindex (Equiv.prodComm m l) (Equiv.prodComm n l)) (Matrix.blockDiagonal fun i => a i • B)
<VAR>α : Type u_2<VAR>m : Type u_9<VAR>n : Type u_10<VAR>NonAssocSemiring α<VAR>DecidableEq m<VAR>DecidableEq n<VAR>a b : ℕ<GOAL>Matrix.kroneckerMap (fun x x_1 => x * x_1) ↑a ↑b = ↑(a * b)
<VAR>α : Type u_2<VAR>l : Type u_8<VAR>m : Type u_9<VAR>n : Type u_10<VAR>NonAssocSemiring α<VAR>DecidableEq n<VAR>A : Matrix l m α<VAR>b : ℕ<GOAL>Matrix.kroneckerMap (fun x x_1 => x * x_1) A ↑b = Matrix.blockDiagonal fun x => b • A
<VAR>α : Type u_2<VAR>l : Type u_8<VAR>m : Type u_9<VAR>n : Type u_10<VAR>NonAssocSemiring α<VAR>DecidableEq l<VAR>a : ℕ<VAR>B : Matrix m n α<GOAL>Matrix.kroneckerMap (fun x x_1 => x * x_1) (↑a) B = (Matrix.reindex (Equiv.prodComm m l) (Equiv.prodComm n l)) (Matrix.blockDiagonal fun x => a • B)
<VAR>α : Type u_2<VAR>l : Type u_8<VAR>m : Type u_9<VAR>n : Type u_10<VAR>Semiring α<VAR>DecidableEq n<VAR>A : Matrix l m α<VAR>b : ℕ<VAR>b.AtLeastTwo<GOAL>Matrix.kroneckerMap (fun x x_1 => x * x_1) A (OfNat.ofNat b) = Matrix.blockDiagonal fun x => MulOpposite.op (OfNat.ofNat b) • A
<VAR>α : Type u_2<VAR>l : Type u_8<VAR>m : Type u_9<VAR>n : Type u_10<VAR>Semiring α<VAR>DecidableEq l<VAR>a : ℕ<VAR>a.AtLeastTwo<VAR>B : Matrix m n α<GOAL>Matrix.kroneckerMap (fun x x_1 => x * x_1) (OfNat.ofNat a) B = (Matrix.reindex (Equiv.prodComm m l) (Equiv.prodComm n l)) (Matrix.blockDiagonal fun x => OfNat.ofNat a • B)
<VAR>α : Type u_2<VAR>m : Type u_9<VAR>n : Type u_10<VAR>MulZeroOneClass α<VAR>DecidableEq m<VAR>DecidableEq n<GOAL>Matrix.kroneckerMap (fun x x_1 => x * x_1) 1 1 = 1
<VAR>α : Type u_2<VAR>l : Type u_8<VAR>m : Type u_9<VAR>n : Type u_10<VAR>MulZeroOneClass α<VAR>DecidableEq n<VAR>A : Matrix l m α<GOAL>Matrix.kroneckerMap (fun x x_1 => x * x_1) A 1 = Matrix.blockDiagonal fun x => A
<VAR>α : Type u_2<VAR>l : Type u_8<VAR>m : Type u_9<VAR>n : Type u_10<VAR>MulZeroOneClass α<VAR>DecidableEq l<VAR>B : Matrix m n α<GOAL>Matrix.kroneckerMap (fun x x_1 => x * x_1) 1 B = (Matrix.reindex (Equiv.prodComm m l) (Equiv.prodComm n l)) (Matrix.blockDiagonal fun x => B)
<VAR>α : Type u_2<VAR>l : Type u_8<VAR>m : Type u_9<VAR>n : Type u_10<VAR>l' : Type u_14<VAR>m' : Type u_15<VAR>n' : Type u_16<VAR>Fintype m<VAR>Fintype m'<VAR>CommSemiring α<VAR>A : Matrix l m α<VAR>B : Matrix m n α<VAR>A' : Matrix l' m' α<VAR>B' : Matrix m' n' α<GOAL>Matrix.kroneckerMap (fun x x_1 => x * x_1) (A * B) (A' * B') = Matrix.kroneckerMap (fun x x_1 => x * x_1) A A' * Matrix.kroneckerMap (fun x x_1 => x * x_1) B B'
<VAR>α : Type u_2<VAR>l : Type u_8<VAR>m : Type u_9<VAR>n : Type u_10<VAR>p : Type u_11<VAR>q : Type u_12<VAR>r : Type u_13<VAR>Semigroup α<VAR>A : Matrix l m α<VAR>B : Matrix n p α<VAR>C : Matrix q r α<GOAL>(Matrix.reindex (Equiv.prodAssoc l n q) (Equiv.prodAssoc m p r)) (Matrix.kroneckerMap (fun x x_1 => x * x_1) (Matrix.kroneckerMap (fun x x_1 => x * x_1) A B) C) = Matrix.kroneckerMap (fun x x_1 => x * x_1) A (Matrix.kroneckerMap (fun x x_1 => x * x_1) B C)
<VAR>α : Type u_2<VAR>l : Type u_8<VAR>m : Type u_9<VAR>n : Type u_10<VAR>p : Type u_11<VAR>q : Type u_12<VAR>r : Type u_13<VAR>Semigroup α<VAR>A : Matrix l m α<VAR>B : Matrix n p α<VAR>C : Matrix q r α<GOAL>(Matrix.kroneckerMap (fun x x_1 => x * x_1) (Matrix.kroneckerMap (fun x x_1 => x * x_1) A B) C).submatrix ⇑(Equiv.prodAssoc l n q).symm ⇑(Equiv.prodAssoc m p r).symm = Matrix.kroneckerMap (fun x x_1 => x * x_1) A (Matrix.kroneckerMap (fun x x_1 => x * x_1) B C)
<VAR>α : Type u_2<VAR>m : Type u_9<VAR>n : Type u_10<VAR>Fintype m<VAR>Fintype n<VAR>Semiring α<VAR>A : Matrix m m α<VAR>B : Matrix n n α<GOAL>(Matrix.kroneckerMap (fun x x_1 => x * x_1) A B).trace = A.trace * B.trace
<VAR>R : Type u_1<VAR>m : Type u_9<VAR>n : Type u_10<VAR>Fintype m<VAR>Fintype n<VAR>DecidableEq m<VAR>DecidableEq n<VAR>CommRing R<VAR>A : Matrix m m R<VAR>B : Matrix n n R<GOAL>(Matrix.kroneckerMap (fun x x_1 => x * x_1) A B).det = A.det ^ Fintype.card n * B.det ^ Fintype.card m
<VAR>R : Type u_1<VAR>m : Type u_9<VAR>n : Type u_10<VAR>Fintype m<VAR>Fintype n<VAR>DecidableEq m<VAR>DecidableEq n<VAR>CommRing R<VAR>A : Matrix m m R<VAR>B : Matrix n n R<GOAL>(Matrix.kroneckerMap (fun x x_1 => x * x_1) A B)⁻¹ = Matrix.kroneckerMap (fun x x_1 => x * x_1) A⁻¹ B⁻¹
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>β : Type u_4<VAR>l : Type u_8<VAR>m : Type u_9<VAR>n : Type u_10<VAR>p : Type u_11<VAR>CommSemiring R<VAR>AddCommMonoid α<VAR>AddCommMonoid β<VAR>Module R α<VAR>Module R β<VAR>A : Matrix l m α<VAR>B : Matrix n p β<VAR>i₁ : l<VAR>i₂ : n<VAR>j₁ : m<VAR>j₂ : p<GOAL>Matrix.kroneckerMap (fun x x_1 => x ⊗ₜ[R] x_1) A B (i₁, i₂) (j₁, j₂) = A i₁ j₁ ⊗ₜ[R] B i₂ j₂
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>β : Type u_4<VAR>l : Type u_8<VAR>m : Type u_9<VAR>n : Type u_10<VAR>p : Type u_11<VAR>CommSemiring R<VAR>AddCommMonoid α<VAR>AddCommMonoid β<VAR>Module R α<VAR>Module R β<VAR>B : Matrix n p β<GOAL>Matrix.kroneckerMap (TensorProduct.tmul R) 0 B = 0
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>β : Type u_4<VAR>l : Type u_8<VAR>m : Type u_9<VAR>n : Type u_10<VAR>p : Type u_11<VAR>CommSemiring R<VAR>AddCommMonoid α<VAR>AddCommMonoid β<VAR>Module R α<VAR>Module R β<VAR>A : Matrix l m α<GOAL>Matrix.kroneckerMap (TensorProduct.tmul R) A 0 = 0
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>l : Type u_8<VAR>m : Type u_9<VAR>n : Type u_10<VAR>p : Type u_11<VAR>CommSemiring R<VAR>AddCommMonoid α<VAR>Module R α<VAR>A₁ A₂ : Matrix l m α<VAR>B : Matrix n p α<GOAL>Matrix.kroneckerMap (TensorProduct.tmul R) (A₁ + A₂) B = Matrix.kroneckerMap (fun x x_1 => x ⊗ₜ[R] x_1) A₁ B + Matrix.kroneckerMap (fun x x_1 => x ⊗ₜ[R] x_1) A₂ B
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>l : Type u_8<VAR>m : Type u_9<VAR>n : Type u_10<VAR>p : Type u_11<VAR>CommSemiring R<VAR>AddCommMonoid α<VAR>Module R α<VAR>A : Matrix l m α<VAR>B₁ B₂ : Matrix n p α<GOAL>Matrix.kroneckerMap (TensorProduct.tmul R) A (B₁ + B₂) = Matrix.kroneckerMap (fun x x_1 => x ⊗ₜ[R] x_1) A B₁ + Matrix.kroneckerMap (fun x x_1 => x ⊗ₜ[R] x_1) A B₂
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>l : Type u_8<VAR>m : Type u_9<VAR>n : Type u_10<VAR>p : Type u_11<VAR>CommSemiring R<VAR>AddCommMonoid α<VAR>Module R α<VAR>r : R<VAR>A : Matrix l m α<VAR>B : Matrix n p α<GOAL>Matrix.kroneckerMap (TensorProduct.tmul R) (r • A) B = r • Matrix.kroneckerMap (fun x x_1 => x ⊗ₜ[R] x_1) A B
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>l : Type u_8<VAR>m : Type u_9<VAR>n : Type u_10<VAR>p : Type u_11<VAR>CommSemiring R<VAR>AddCommMonoid α<VAR>Module R α<VAR>r : R<VAR>A : Matrix l m α<VAR>B : Matrix n p α<GOAL>Matrix.kroneckerMap (TensorProduct.tmul R) A (r • B) = r • Matrix.kroneckerMap (fun x x_1 => x ⊗ₜ[R] x_1) A B
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>m : Type u_9<VAR>n : Type u_10<VAR>CommSemiring R<VAR>AddCommMonoid α<VAR>Module R α<VAR>DecidableEq m<VAR>DecidableEq n<VAR>a : m → α<VAR>b : n → α<GOAL>Matrix.kroneckerMap (TensorProduct.tmul R) (Matrix.diagonal a) (Matrix.diagonal b) = Matrix.diagonal fun mn => a mn.1 ⊗ₜ[R] b mn.2
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>l : Type u_8<VAR>m : Type u_9<VAR>n : Type u_10<VAR>CommSemiring R<VAR>AddCommMonoid α<VAR>Module R α<VAR>DecidableEq n<VAR>A : Matrix l m α<VAR>b : n → α<GOAL>Matrix.kroneckerMap (TensorProduct.tmul R) A (Matrix.diagonal b) = Matrix.blockDiagonal fun i => A.map fun a => a ⊗ₜ[R] b i
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>l : Type u_8<VAR>m : Type u_9<VAR>n : Type u_10<VAR>CommSemiring R<VAR>AddCommMonoid α<VAR>Module R α<VAR>DecidableEq l<VAR>a : l → α<VAR>B : Matrix m n α<GOAL>Matrix.kroneckerMap (TensorProduct.tmul R) (Matrix.diagonal a) B = (Matrix.reindex (Equiv.prodComm m l) (Equiv.prodComm n l)) (Matrix.blockDiagonal fun i => B.map fun b => a i ⊗ₜ[R] b)
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>β : Type u_4<VAR>γ : Type u_6<VAR>l : Type u_8<VAR>m : Type u_9<VAR>n : Type u_10<VAR>p : Type u_11<VAR>q : Type u_12<VAR>r : Type u_13<VAR>CommSemiring R<VAR>AddCommMonoid α<VAR>AddCommMonoid β<VAR>AddCommMonoid γ<VAR>Module R α<VAR>Module R β<VAR>Module R γ<VAR>A : Matrix l m α<VAR>B : Matrix n p β<VAR>C : Matrix q r γ<GOAL>(Matrix.reindex (Equiv.prodAssoc l n q) (Equiv.prodAssoc m p r)) ((Matrix.kroneckerMap (TensorProduct.tmul R) (Matrix.kroneckerMap (TensorProduct.tmul R) A B) C).map ⇑(TensorProduct.assoc R α β γ)) = Matrix.kroneckerMap (TensorProduct.tmul R) A (Matrix.kroneckerMap (TensorProduct.tmul R) B C)
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>β : Type u_4<VAR>γ : Type u_6<VAR>l : Type u_8<VAR>m : Type u_9<VAR>n : Type u_10<VAR>p : Type u_11<VAR>q : Type u_12<VAR>r : Type u_13<VAR>CommSemiring R<VAR>AddCommMonoid α<VAR>AddCommMonoid β<VAR>AddCommMonoid γ<VAR>Module R α<VAR>Module R β<VAR>Module R γ<VAR>A : Matrix l m α<VAR>B : Matrix n p β<VAR>C : Matrix q r γ<GOAL>((Matrix.kroneckerMap (TensorProduct.tmul R) (Matrix.kroneckerMap (TensorProduct.tmul R) A B) C).map ⇑(TensorProduct.assoc R α β γ)).submatrix ⇑(Equiv.prodAssoc l n q).symm ⇑(Equiv.prodAssoc m p r).symm = Matrix.kroneckerMap (TensorProduct.tmul R) A (Matrix.kroneckerMap (TensorProduct.tmul R) B C)
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>β : Type u_4<VAR>m : Type u_9<VAR>n : Type u_10<VAR>CommSemiring R<VAR>AddCommMonoid α<VAR>AddCommMonoid β<VAR>Module R α<VAR>Module R β<VAR>Fintype m<VAR>Fintype n<VAR>A : Matrix m m α<VAR>B : Matrix n n β<GOAL>(Matrix.kroneckerMap (TensorProduct.tmul R) A B).trace = A.trace ⊗ₜ[R] B.trace
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>m : Type u_9<VAR>n : Type u_10<VAR>CommSemiring R<VAR>Semiring α<VAR>Algebra R α<VAR>DecidableEq m<VAR>DecidableEq n<GOAL>Matrix.kroneckerMap (TensorProduct.tmul R) 1 1 = 1
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>β : Type u_4<VAR>l : Type u_8<VAR>m : Type u_9<VAR>n : Type u_10<VAR>l' : Type u_14<VAR>m' : Type u_15<VAR>n' : Type u_16<VAR>CommSemiring R<VAR>Semiring α<VAR>Semiring β<VAR>Algebra R α<VAR>Algebra R β<VAR>Fintype m<VAR>Fintype m'<VAR>A : Matrix l m α<VAR>B : Matrix m n α<VAR>A' : Matrix l' m' β<VAR>B' : Matrix m' n' β<GOAL>Matrix.kroneckerMap (TensorProduct.tmul R) (A * B) (A' * B') = Matrix.kroneckerMap (TensorProduct.tmul R) A A' * Matrix.kroneckerMap (TensorProduct.tmul R) B B'