no goals
l : Type ?u.487731
m : Type ?u.487734
n : Type u_1
o : Type ?u.487740
m' : o → Type ?u.487745
n' : o → Type ?u.487750
R : Type ?u.487753
S : Type ?u.487756
α : Type v
β : Type w
γ : Type ?u.487763
inst✝² : CommSemiring α
inst✝¹ : Fintype n
inst✝ : DecidableEq n
r : α
M : Matrix n n α
⊢ Commute (↑(scalar n) r) M
simp [Commute, SemiconjBy]