Block diagonal matrices with unequally size blocks

Stream: general

[Eric Wieser]

We currently have docs#matrix.block_diagonal, which produces rectangular matrices matrix (m × o) (n × o) α consisting of a diagonal of equally-sized matrix m n blocks.

I'm finding myself wanting a depedently-typed version matrix (Σ i, m i) (Σ i, n i) α so that I can define the jordan canonical form, and have something like:

variables {α : Type*} [has_zero α]
variables {o : Type*} [fintype o] [decidable_eq o]
variables {n : o → Type*} [∀ i, fintype (n i)] [∀ i, decidable_eq (n i)]
variables {m : o → Type*} [∀ i, fintype (m i)] [∀ i, decidable_eq (m i)]
variables (M N : Π i, matrix (m i) (n i) α) [decidable_eq o]

def block_diagonal : matrix (Σ i, m i) (Σ i, n i) α
| ⟨k, i⟩ ⟨k', j⟩ := if h : k = k' then M k i (cast (congr_arg n h.symm) j) else 0

Should this Σ version replace the × version (assuming I can fix all the uses)? If not, what should it be called?

[Eric Wieser]

#7068 adds this under the primed name.