mathlib3

6db70c98 - refactor(linear_algebra/determinant): refactor proof of upper_two_block_triangular_det (#6690)

refactor(linear_algebra/determinant): refactor proof of upper_two_block_triangular_det (#6690) Refactored the proof of upper_two_block_triangular_det (to use sum_congr_hom.range) following a suggestion from Eric Wieser (during PR review of #6050). Co-authored-by: paulvanwamelen <30371019+paulvanwamelen@users.noreply.github.com> Co-authored-by: Eric Wieser <wieser.eric@gmail.com>