Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-03-17 19:18 6db70c98

View on Github →

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).

Estimated changes