mathlib

9c861e32 - feat(topology/algebra/matrix): `matrix.block_diagonal` is continuous (#13641)

feat(topology/algebra/matrix): `matrix.block_diagonal` is continuous (#13641) `continuous.if_const` isn't suitable for the primed `matrix.block_diagonal'` case, as the `if` is dependent.