no goals
l : Type ?u.972645
m : Type u_2
n : Type u_3
o : Type ?u.972654
m' : o → Type ?u.972659
n' : o → Type ?u.972664
R : Type u_1
S : Type ?u.972670
α : Type v
β : Type w
γ : Type ?u.972677
inst✝³ : Star R
inst✝² : Star α
inst✝¹ : SMul R α
inst✝ : SMul Rᵐᵒᵖ α
c : R
M : Matrix m n α
h : ∀ (r : R) (a : α), star (r • a) = MulOpposite.op (star r) • star a
⊢ ∀ (i : n) (j : m), (c • M)ᴴ i j = (MulOpposite.op (star c) • Mᴴ) i j
simp [h]