no goals
m : Type ?u.1669131
n : Type u_1
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
A B C : Matrix n n R
hC : det C = 1
hA : A = C ⬝ B
⊢ det C * det B = det B
rw [hC, one_mul]