no goals
m : Type ?u.1667151
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 = B ⬝ C
⊢ det B * det C = det B
rw [hC, mul_one]