no goals
l : Type ?u.356623
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B : Matrix n n α
⊢ (List.prod [])⁻¹ = List.prod (List.map Inv.inv (List.reverse []))
rw [List.reverse_nil, List.map_nil, List.prod_nil, inv_one]
no goals
l : Type ?u.356623
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A✝ B A : Matrix n n α
Xs : List (Matrix n n α)
⊢ (List.prod (A :: Xs))⁻¹ = List.prod (List.map Inv.inv (List.reverse (A :: Xs)))
rw [List.reverse_cons', List.map_concat, List.prod_concat, List.prod_cons, Matrix.mul_eq_mul,
  Matrix.mul_eq_mul, mul_inv_rev, list_prod_inv_reverse Xs]