no goals
l : Type ?u.1009478
m : Type u_2
n : Type u_3
o : Type ?u.1009487
m' : o → Type ?u.1009492
n' : o → Type ?u.1009497
R : Type u_1
S : Type ?u.1009503
α : Type v
β : Type w
γ : Type ?u.1009510
inst✝³ : DivisionSemiring R
inst✝² : AddCommMonoid α
inst✝¹ : StarAddMonoid α
inst✝ : Module R α
c : ℕ
M : Matrix m n α
⊢ ∀ (i : n) (j : m), ((↑c)⁻¹ • M)ᴴ i j = ((↑c)⁻¹ • Mᴴ) i j
simp