no goals
l : Type ?u.411237
m : Type u
n : Type u'
α : Type v
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : CommRing α
A B : Matrix n n α
inst✝¹ : Fintype m
inst✝ : DecidableEq m
M : Matrix m m α
h : IsUnit M
N : Matrix m m α
⊢ det (M⁻¹ ⬝ N ⬝ M) = det N
rw [← h.unit_spec, ← coe_units_inv, det_units_conj']