no goals
k : Type u_2
l : Type ?u.76298
m : Type u_3
n : Type u_1
α : Type v
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : DecidableEq k
inst✝¹ : DecidableEq m
inst✝ : Semiring α
b₁ b₂ : n
hb : b₁ ≠ b₂
a : m
c : k
⊢ toMatrix (single a b₁) ⬝ toMatrix (single b₂ c) = 0
rw [← toMatrix_trans, single_trans_single_of_ne hb, toMatrix_bot]