mathlib3

2deda90e - feat(data/fin): help `simp` reduce expressions containing `fin.succ_above` (#7308)

feat(data/fin): help `simp` reduce expressions containing `fin.succ_above` (#7308) With these `simp` lemmas, in combination with #6897, `simp; ring` can almost automatically compute the determinant of matrices like `![![a, b], ![c, d]]`. Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>