From efef0f938c63424530912d0cef2421e6d7e789c5 Mon Sep 17 00:00:00 2001 From: Alex J Best Date: Mon, 8 Jan 2024 15:16:24 +0000 Subject: [PATCH] break --- test/matrix.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/test/matrix.lean b/test/matrix.lean index 373088b059c88..33a418b54347c 100644 --- a/test/matrix.lean +++ b/test/matrix.lean @@ -139,7 +139,7 @@ example {α : Type _} [CommRing α] {a b c d : α} : simp only [det_succ_row_zero, of_apply, cons_val', empty_val', cons_val_fin_one, cons_val_zero, det_unique, Fin.default_eq_zero, submatrix_apply, Fin.succ_zero_eq_one, cons_val_one, head_fin_const, Fin.sum_univ_succ, Fin.val_zero, - pow_zero, one_mul, Fin.zero_succAbove, head_cons, Finset.univ_unique, + pow_zero, one_mul, Fin.zero_succAbove, Finset.univ_unique, Fin.val_succ, Fin.coe_fin_one, zero_add, pow_one, cons_val_succ, neg_mul, Fin.succ_succAbove_zero, Finset.sum_const, Finset.card_singleton, smul_neg, one_smul] ring