l m n : ℕ
α : Type u_1
β : Type ?u.30925
inst✝¹ : Mul α
inst✝ : AddCommMonoid α
A : Matrix (Fin l) (Fin m) α
B : Matrix (Fin m) (Fin n) α
⊢ (↑of fun x x_1 => A x ⬝ᵥ ↑of (fun x y => B y x) x_1) = fun i k => (fun j => A i j) ⬝ᵥ fun j => B j k
l m n : ℕ
α : Type u_1
β : Type ?u.30925
inst✝¹ : Mul α
inst✝ : AddCommMonoid α
A : Matrix (Fin l) (Fin m) α
B : Matrix (Fin m) (Fin n) α
⊢ mulᵣ A B = A ⬝ B
simp [mulᵣ, Function.comp, Matrix.mul, Matrix.transpose]
no goals
l m n : ℕ
α : Type u_1
β : Type ?u.30925
inst✝¹ : Mul α
inst✝ : AddCommMonoid α
A : Matrix (Fin l) (Fin m) α
B : Matrix (Fin m) (Fin n) α
⊢ (↑of fun x x_1 => A x ⬝ᵥ ↑of (fun x y => B y x) x_1) = fun i k => (fun j => A i j) ⬝ᵥ fun j => B j k
rfl